Math/pad is a document preparation system designed and developed by the authors and oriented towards the calculational construction of programs. PVS (Prototype Verification System) is a theorem checker developed at SRI that has been extensively used for verifying software, in particular in safety-critical applications. This paper describes how these two systems have been combined into one. We discuss the potential benefits of the combination seen from the viewpoint of someone wanting to use formal methods for the construction of computer programs, and we discuss the architecture of the combined system for the benefit of anyone wanting to investigate combining the Math/pad system with other programming tools.
CITATION STYLE
Verhoeven, R., & Backhouse, R. (1999). Interfacing program construction and verification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1709, pp. 1128–1146). Springer Verlag. https://doi.org/10.1007/3-540-48118-4_10
Mendeley helps you to discover research relevant for your work.