| | | | |
|

The PVS Proof Checker: A Reference Manual (Beta Release)
by Sam Owre, Dr. John Rushby & Dr. Natarajan Shankar.
Abstract
PVS stands for "Prototype Verification System," and as the name suggests, it is a prototype for a system for specification and verification based on higher-order logic.1 The present document is a reference manual for the commands employed in constructing proofs using the PVS proof checker. The PVS User Guide [OSR93b] should be consulted for information on how to use the system to develop specifications and proofs. The PVS Language Reference [OSR93a] describes the language of PVS. The PVS Tutorial [SOR93] provides an introduction to the entire system.
Files
|
|
|