D-Finder: A Tool for Compositional Deadlock Detection and Verification

  • Saddek Bensalem
  • Marius Bozga
  • Thanh-Hung Nguyen
  • Joseph Sifakis
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)


D-Finder tool implements a compositional method for the verification of component-based systems described in BIP language encompassing multi-party interaction. For deadlock detection, D-Finder applies proof strategies to eliminate potential deadlocks by computing increasingly stronger invariants.


Model Check Atomic Component Compositional Method Strong Invariant Component Invariant 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Alur, R., Henzinger, T.: Reactive modules. In: Proceedings of the 11th Annual Symposium on LICS, pp. 207–208. IEEE Computer Society Press, Los Alamitos (1996)Google Scholar
  2. 2.
    Abadi, M., Lamport, L.: Conjoining specifications. Toplas 17(3), 507–534 (1995)CrossRefGoogle Scholar
  3. 3.
    Clarke, E., Long, D., McMillan, K.: Compositional model checking. In: Proceedings of the 4th Annual Symposium on LICS, pp. 353–362 (1989)Google Scholar
  4. 4.
    Chandy, K., Misra, J.: Parallel program design: a foundation. Addison-Wesley Publishing Company, Reading (1988)zbMATHGoogle Scholar
  5. 5.
    Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Transactions on Programming Languages and Systems 16(3), 843–871 (1994)CrossRefGoogle Scholar
  6. 6.
    McMillan, K.L.: A compositional rule for hardware design refinement. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 24–35. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  7. 7.
    Pnueli, A.: In transition from global to modular temporal reasoning about programs, pp. 123–144 (1985)Google Scholar
  8. 8.
    Stark, E.W.: A proof technique for rely/guarantee properties. In: Maheshwari, S.N. (ed.) FSTTCS 1985. LNCS, vol. 206, pp. 369–391. Springer, Heidelberg (1985)CrossRefGoogle Scholar
  9. 9.
    Kupferman, O., Vardi, M.Y.: Modular model checking. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 381–401. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  10. 10.
    Peterson, J.: Petri Net theory and the modelling of systems. Prentice Hall, Englewood Cliffs (1981)zbMATHGoogle Scholar
  11. 11.
    Apt, K.R., Francez, N., de Roever, W.P.: A proof system for communicating sequential processes. ACM Trans. Program. Lang. Syst. 2(3), 359–385 (1980)CrossRefzbMATHGoogle Scholar
  12. 12.
    Basu, A., Bozga, M., Sifakis, J.: Modeling heterogeneous real-time components in bip. In: SEFM, pp. 3–12 (2006)Google Scholar
  13. 13.
    Lakhnech, Y., Bensalem, S., Berezin, S., Owre, S.: Incremental verification by abstraction. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 98–112. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  14. 14.
    Bradley, A.R., Manna, Z.: Checking safety by inductive generalization of counterexamples to induction. In: FMCAD, pp. 173–180 (2007)Google Scholar
  15. 15.
    Bensalem, S., Lakhnech, Y.: Automatic generation of invariants. FMSD 15(1), 75–92 (1999)Google Scholar
  16. 16.
    Bensalem, S., Bozga, M., Sifakis, J., Nguyen, T.H.: Compositional verification for component-based systems and application. In: Cha, S., Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 64–79. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  17. 17.
    Team, O.: The omega library. Version 1.1.0 (1996)Google Scholar
  18. 18.
    Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  19. 19.
    Cobleigh, J.M., Avrunin, G.S., Clarke, L.A.: Breaking up is hard to do: An evaluation of automated assume-guarantee reasoning. ACM TSEM 17(2) (2008)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Saddek Bensalem
    • 1
  • Marius Bozga
    • 1
  • Thanh-Hung Nguyen
    • 1
  • Joseph Sifakis
    • 1
  1. 1.Verimag LaboratoryUniversité Joseph Fourier Grenoble, CNRSFrance

Personalised recommendations