| | | | |
|

The PVS Specification Language (Beta Release)
by Sam Owre, Dr. John Rushby & Dr. Natarajan Shankar.
Abstract
PVS is a Prototype Verification System for specifying and verifying digital systems. The PVS system consists of a specification language, a parser, a typechecker, a prover, specification libraries, and various browsing tools. This document primarily describes the specification language and is meant to be used as a reference manuaL The PVS User Guide [9] is to be consulted for information on how to use the system to develop specifications and proofs, The PVS Proof Checker manual [11] is a reference manual for the commands used to construct proofs.
Files
|
|
|