There is extensive PVS documentation, including PVS Manuals, Tutorials, Papers, and a PVS bibliography.
Note: these manuals are largely out of date. For the most part, they are still correct, but there are new features not covered in them. The release notes describe the differences, and should be consulted.
To effectively use PVS, you should at least get the System Guide, Language Reference, and Prover Guide. 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.
The PDF files have live links and are better for online viewing, while the postscript files are better for printing since there are no colors involved.
| ps | ps.gz | specs | ||
|---|---|---|---|---|
| System Guide | |
|
|
|
| Language Reference |
|
|
|
|
| Prover Guide |
|
|
|
|
| Prelude |
|
|
|
|
| Semantics |
|
|
|
|
| Datatypes |
|
|
|
specs |
| Theory Interpretations |
|
|
|
|
| Release Notes |
|
|
N/A |
Here are links to some features whose documentation has not yet made it to the above manuals:
The following links lead to directories of examples and tutorials relating to PVS. Each directory contains documentation and PVS dump files, which contain the specifications and proofs related in each example, allowing you to follow them on your workstation.
To undump PVS .dmp files, copy them 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.
Note that these specifications and proofs have not yet been updated to PVS 2.3 or later, so use with caution!
The best place to start is the The standard introductory tutorial to PVS (WIFT).
Another good source of examples of PVS specifications and proofs is the PVS Libraries.
We maintain a citations database for papers which reference the history, technology and applications of PVS, which currently contains over 300 citations. Please tell us about new papers by filling in this form, or send email to pvs-sri@csl.sri.com. (Please read these suggestions about publishing on the Web first!)
Note: This bibliography is no longer actively maintained, though we will update it on request - just fill in the above form or send your bibliography entries to mailto:pvs-sri@csl.sri.com.
The database is available for downloading in the following formats: