Abstract
Formal specification and verification techniques can improve the quality of programs by enabling the analysis and proof of semantic program properties. This paper describes the modular architecture of an interactive program prover that we are currently developing for a Java subset. In particular, it discusses the integration of a programming language-specific prover component with a general purpose theorem prover.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
B. Buth. An interface between Pamela and PVS. Technical report, Universität Bremen, 1997. Available from http://www.informatik.uni-bremen.de/~bb/bb.html 76
Computer Science Department, Stanford University. Stanford PASCAL Verifier-User Manual, 1979. 66
COR+95._J. Crow, S. Owre, J. Rushby, N. Shankar, and M. Srivas. A Tutorial Introduction to PVS, April 1995. 65
D. L. Detlefs, K. R. M. Leino, G. Nelson, and J. B. Saxe. Extended static checking. Research Report 159, Digital Systems Research Center, 1998. 66
J. V. Guttag and J. J. Horning. Larch: Languages and Tools for Formal Specification. Texts and Monographs in Computer Science. Springer-Verlag, 1993. 64
D. Guaspari, C. Marceau, and W. Polak. Formal verification of Ada programs. IEEE Transactions on Software Engineering, 16(9):1058–1075, September 1990. 66
M. J. C. Gordon. Mechanizing programming logics in higher order logic. In G. Birtwistle and P.A. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving. Springer-Verlag, 1989. Kopiensammlung. 66
B. Jacobs, J. van den Berg, M. Huisman, M. van Berkum, U. Hensel, and H. Tews. Reasoning about Java classes. In Proceedings of Object-Oriented Programming Systems, Languages and Applications (OOPSLA), 1998. Also available as TR CSI-R9812, University of Nijmegen. 65
P. Müller and A. Poetzsch-Heffter. Modular specification and verification techniques for object-oriented software components. In G. Leavens and M. Sitaraman, editors, Foundations of Component-Based Systems. Cambridge University Press, 1999. 65, 68
S.S. Owicki. Axiomatic proof techniques for parallel programs. Technical report, Computer Science Dept., 1975. 72
Lawrence C. Paulson. Isabelle: a generic theorem prover, volume 828 of Lecture Notes in Computer Science. Springer-Verlag Inc., New York, NY, USA, 1994. 65
A. Poetzsch-Heffter. Prototyping realistic programming languages based on formal specifications. Acta Informatica, 34:737–772, 1997. 75
A. Poetzsch-Heffter. Specification and verification of object-oriented programs. Habilitation thesis, Technical University of Munich, January 1997. 65
A. Poetzsch-Heffter and P. Müller. A programming logic for sequential Java. In D. Swierstra, editor, ESOP’ 99, LNCS 1576. Springer-Verlag, 1999. 69, 73
Terence J. Parr and Russell W. Quong. ANTLR: A predicated-LL(k) parser generator. Software—Practice and Experience, 25(7):789–810, July 1995. 75
W. Reif. The KIV approach to software verification. In M. Broy and S. Jähnichen, editors, Korso: Methods, Languages, and Tools for the Construction of Correct Software, volume 1009 of Lecture Notes in Computer Science. Springer-Verlag, 1995. 66
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Meyer, J., Poetzsch-Heffter, A. (2000). An Architecture for Interactive Program Provers. In: Graf, S., Schwartzbach, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2000. Lecture Notes in Computer Science, vol 1785. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46419-0_6
Download citation
DOI: https://doi.org/10.1007/3-540-46419-0_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67282-1
Online ISBN: 978-3-540-46419-8
eBook Packages: Springer Book Archive