PVS Manuals
This page collects the essential resources to get started with PVS.
- System Guide: this document presents the PVS architecture and the commands needed to create, edit, and verify PVS models.
- Language Reference: this document introduces the syntax of the PVS modelling language.
- Prover Guide: this document describes the commands for interacting with the PVS theorem prover.
- PVSio Manual: this document describes the commands for interacting with the PVSio animation environment.
- PVSio-web Manual: this document describes how to use the PVSio-web rapid prototyping environment.
PVS Advanced Features
The semantics report provides the semantics for the core of PVS, the datatypes report provides details and examples that go beyond what is described in the language manual, and theory interpretations describes the recently introduced capabilities supporting refinement and consistency.
Libraries
A PVS library is a directory containing PVS theories and proofs for concepts that have some wider use. Research groups have developed several libraries, but over the years most have been consolidated into either the PVS Prelude or the NASA Librarysince these are fully maintained. The PVS Prelude is the standard library built in to the PVS system. It is preloaded automatically every time PVS is executed. It provides standard definitions, ranging from common base types (bool, integer,real, etc.) to functions, set, relations, lists and many more. The NASA Library is a massive library developed and maintained by the the NASA Langley Formal Methods team. It includes definitions and theorems for algebra, analysis, graphs, series, and trigonometric functions, among others.
PVS Tutorials and Examples
The following links lead to tutorials and examples relating to PVS. For some examples we made available a PVS dump files, which contain the specifications and proofs presented in the example, allowing you to follow them on your workstation. To open a PVS dump file (.dmp), copy the file into a new directory and issue the command M-x undump-pvs-files from within PVS. After typechecking, you can then step through the proofs with M-x step-proof and TAB-1.