Abstract
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 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 a failed search for counterexamples, we can generate a fully deductive proof that the system meets its specification.
Cite
CITATION STYLE
Peled, D., Pnueli, A., & Zuck, L. (2001). From falsification to verification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2245, pp. 292–304). Springer Verlag. https://doi.org/10.1007/3-540-45294-x_25
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
