From Falsification to Verification
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.
- 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.E.A. Emerson and E.M. Clarke. Characterizingcorrectness properties of parallel programs using fixpoints. In ICALP’80, pp. 169–181, LNCS 85.Google Scholar
- 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.O. Lichtenstein, A. Pnueli, and L. Zuck. The glory of the past. In LICS’85, LNCS 193, pp. 196–218, 1985.Google Scholar
- 8.Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995.Google Scholar
- 9.K.S. Namjoshi. Certifyingmo del checkers. In CAV’01, LNCS 2102, pp. 2–13.Google Scholar
- 10.D. Peled and L. Zuck. From model checkingto a temporal proof. In SPIN’2001, LNCS 2057pp. 1–14.Google Scholar
- 11.M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In LICS’86, pp. 332–344, 1986.Google Scholar