From Falsification to Verification

  • Doron Peled
  • Amir Pnueli
  • Lenore Zuck
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2245)


This paper enhances the linear temporal logic model checking process with the ability to automatically generate a deductive proof that the system meets its temporal specification. Thus, we emphasize the point of view that model checkingcan also be used to justify why the system actually works. We show that, by exploitingthe information in the graph that is generated during a failed search for counterexamples, we can generate a fully deductive proof that the system meets its specification.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    E.M. Clarke and E.A. Emerson. Design and synthesis of synchronization skeletons usingbranc hingtime temporal logic. In Proc. IBM Workshop on Logics of Programs, LNCS 131, 1981.Google Scholar
  2. 2.
    E.A. Emerson and E.M. Clarke. Characterizingcorrectness properties of parallel programs using fixpoints. In ICALP’80, pp. 169–181, LNCS 85.Google Scholar
  3. 3.
    Y. Kesten and A. Pnueli. Verification by finitary abstraction. Information and Computation, 163:203–243, 2000.zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    R.P. Kurshan. Computer Aided Verification of Coordinating Processes. Princeton University Press, Princeton, New Jersey, 1995.zbMATHGoogle Scholar
  5. 5.
    O. Lichtenstein and A. Pnueli. Checkingthat finite-state concurrent programs satisfy their linear specification. In POPL’85, pp. 97–107, 1985.Google Scholar
  6. 6.
    O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In LICS’85, LNCS 193, pp. 196–218, 1985.Google Scholar
  7. 7.
    Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1991.zbMATHGoogle Scholar
  8. 8.
    Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995.Google Scholar
  9. 9.
    K.S. Namjoshi. Certifyingmo del checkers. In CAV’01, LNCS 2102, pp. 2–13.Google Scholar
  10. 10.
    D. Peled and L. Zuck. From model checkingto a temporal proof. In SPIN’2001, LNCS 2057pp. 1–14.Google Scholar
  11. 11.
    M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In LICS’86, pp. 332–344, 1986.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Doron Peled
    • 1
  • Amir Pnueli
    • 2
  • Lenore Zuck
    • 3
  1. 1.Univeristy of TexasUSA
  2. 2.Weizmann Institute of ScienceRehovotIsrael
  3. 3.New York UniversityNew York

Personalised recommendations