There is extensive PVS documentation, including PVS Manuals, Tutorials, Papers, and a PVS bibliography.

PVS Manuals

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.

pdf ps ps.gz specs
System Guide PDF PS PS.GZ
Language Reference PDF PS PS.GZ
Prover Guide PDF PS PS.GZ
Prelude PDF PS PS.GZ
Semantics PDF PS PS.GZ
Datatypes PDF PS PS.GZ specs
Theory Interpretations PDF PS PS.GZ
Release Notes PDF PS N/A

Here are links to some features whose documentation has not yet made it to the above manuals:

PVS Tutorials

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.

PVS papers

The following is a partial list of some of the more important papers about PVS that we have written.
Other papers pertaining to PVS and related topics are kept (more or less) current by their owners:

PVS Bibliography

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

The database is available for downloading in the following formats: