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
PS
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