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.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Bergstra, J. A., Klop, J. W. Proving Program Inclusion Using HOARE's Logic, Theoretical Computer Science 30 (1984), pp. 1–48
Boyer, R.S./ Moore, J.S. A Computational Logic. Academic Press, New York 1979
Burstall, R.M. Program Proving as Hand Simulation with a little Induction. Information Processing 74, North-Holland Publishing Company (1974)
Bundy, A. Automatic Guidance of Program Synthesis Proofs. Proc. Workshop on Automating Software Design, IJCAI 89. Kestrel Institute, Palo Alto (1989), pp. 57–59
Constable, R. et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice Hall, Englewood Cliffs (1986)
E.W. Dijkstra. Lecture held on 8/4/1988, International Summer School "Constructive Methods in Computing Science", Marktoberdorf 1988.
Felty, A./Miller, D. Specifying Theorem Provers in a Higher-Oder Logic Programming Language. Proc. 9-th International Conference on Automated Deduction, E. Lusk, R. Overbeek (eds), Springer LNCS 310 (1988), pp. 61–80
Gordon,M/Milner,R./Wadsworth,C. Edinburgh LCF. Springer LNCS 78 (1979)
Goldblatt, R. Axiomatising the Logic of Computer Programming. Springer LNCS 130 (1982)
Gries, D. The Science of Programming, Springer-Verlag (1981)
Harel, D. First Order Dynamic Logic. Springer LNCS 68 (1979)
Hähnle, R. Programmverifikation durch symbolische Ausführung und Induktion. Diplomarbeit, Fakultät für Informatik, Universität Karlsruhe (1987)
Heisel, M. A Formalization and Implementation of Gries's Program Development Method within the KIV Environment. Int. Bericht 3/89, Fak. für Informatik, Univ. Karlsruhe
Heisel,M./Reif, W./Stephan, W. Program Verification by Symbolic Execution and Induction. Proc. 11-th German Workshop on Artificial Intelligence, K. Morik (ed.), Informatik Fachberichte 152, Springer-Verlag (1987)
Heisel, M./Reif, W./Stephan, W. A Dynamic Logic for Program Verification. Proc. Logic at Botik 89, A. Meyer, M. Taitslin (eds), Springer LNCS 363 (1989), pp. 134–145
Mulmuly, K. Mechanization of existence proofs of recursive functions. Proc. 7-th International Conference on Automated Deduction, Springer LNCS 170 (1984), pp. 460–475
Oppacher, F./Suen, E. HARP: A Tableau-Based Theorem Prover. Journal of Automated Reasoning, Vol. 4 (1988), pp. 69–100.
Paulson, L. Logic and computation. Cambridge University Press, Cambridge (1987)
Reif, W. Vollständigkeit einer modifizierten Goldblatt-Logik und Approximation der Omegaregel durch Induktion. Diplomarbeit, Fak. für Informatik, Univ. Karlsruhe (1984)
Stephan, W. A Logic for Recursive Programs. Interner Bericht 5/85, Fak. für Informatik, Universität Karlsruhe (1985)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Heisel, M., Reif, W., Stephan, W. (1990). Tactical theorem proving in program verification. In: Stickel, M.E. (eds) 10th International Conference on Automated Deduction. CADE 1990. Lecture Notes in Computer Science, vol 449. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52885-7_83
Download citation
DOI: https://doi.org/10.1007/3-540-52885-7_83
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52885-2
Online ISBN: 978-3-540-47171-4
eBook Packages: Springer Book Archive