Writing PVS Proof Strategies

Sam Owre and N. Shankar
Design and Application of Strategies/Tactics in Higher Order Logics (STRATA 2003)

Abstract

PVS (Prototype Verification System) is a comprehensive framework for writing formal logical specifications and constructing proofs. An interactive proof checker is a key component of PVS. The capabilities of this proof checker can be extended by defining proof strategies that are similar to LCF-style tactics. Commonly used proof strategies include those for discharging typechecking proof obligations, simplification and rewriting using decision procedures, and various forms of induction. We describe the basic building blocks of PVS proof strategies and provide a pragmatic guide for writing sophisticated strategies.

PDF PS

Slides

PDF

BibTeX Entry

@inproceedings{pvs-strategies:STRATA03,
	AUTHOR = {Sam Owre and N. Shankar},
	TITLE = {Writing {PVS} Proof Strategies},
        BOOKTITLE = {Design and Application of Strategies/Tactics in
	             Higher Order Logics (STRATA 2003)},
	EDITOR = {Myla Archer and Ben Di Vito and C\'{e}sar Mu{\~{n}}oz},
	PAGES = {1--15},
        MONTH = sep,
        YEAR = 2003,
        PUBLISHER = {NASA Langley Research Center},
        ADDRESS = {Hampton, VA},
	SERIES = {NASA Conference Publication},
	NUMBER = {CP-2003-212448},
	NOTE = {The complete proccedings are available at
	        \url{http://research.nianet.org/fm-at-nia/STRATA2003/}}
}

Sam Owre: owre@csl.sri.com