Abstract
A “shell” for program verification and development is presented which is obtained by using a variant of Dynamic Logic in combination with tactical theorem proving. This shell (Karlsruhe Interactive Verifier) allows easy implementations of various strategies which are guaranteed to be correct with respect to the basic logic. It is shown how tactical theorem proving is adapted for the above purposes.
Cite
CITATION STYLE
Heisel, M., Reif, W., & Stephan, W. (1990). Tactical theorem proving in program verification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 449 LNAI, pp. 117–131). Springer Verlag. https://doi.org/10.1007/3-540-52885-7_83
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
