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 specfication. Thus, we emphasize the point of view that model checking can also be used to justify why the system actually works. We show that, by exploiting the information in the graph that is generated during the search for counterexamples, when the search of counterexamples fails, we can generate a fully deductive proof that the system meets its specification.
Proc. 21th Conference on the Foundations of Software Technology and Theoretical Computer Science