Interfacing program construction and verification

P.H.F.M. Verhoeven, R.C. Backhouse

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

7 Citations (Scopus)


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.
Original languageEnglish
Title of host publicationFM'99 - Formal Methods (Proceedings World Congress on Formal Methods in the Development of Computing Systems, Toulouse, France, September 20-24, 1999)
EditorsJ.M. Wing, J. Woodcock, J. Davies
Place of PublicationBerlin
ISBN (Print)3-540-66588-9
Publication statusPublished - 1999

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Dive into the research topics of 'Interfacing program construction and verification'. Together they form a unique fingerprint.

Cite this