PVS has had many developments since it was first officially introduced in 1996, and the manuals have not kept up. For the most part, the system is backward-compatible, so the documentation is still accurate. However, many important new features of PVS are only mentioned in the Release Notes.
If you're new to PVS, we suggest you start with the the system guide tour. This will give you a quick feel for the system and it's basic capabilities. After that it depends on your goals and interests.
There is extensive PVS documentation, divided below into sections:
Release Notes cover versions of PVS from 3.0 to 7.1, they describe new features, bug fixes, etc. It is worth skimming, as many useful new features of PVS are only described in the release notes.
System Guide has a tour of the most used features of PVS, along with the commands, files, and operating system interaction. PVS was originally written with an Emacs GUI, and this is described here.
vscode-pvs is a newer GUI for PVS, based on Microsoft Visual Studio code, that is being actively developed by NASA as an alternative to Emacs. Both GUIs will be supported in PVS in the future, so choose either or both.
PVS: A Prototype Verification System by Sam Owre, Natarajan Shankar, and John Rushby, from CADE 11, Saratoga Springs, NY, June 1992. One of the earliest descriptions of the PVS system.
PVS: An Experience Report by Sam Owre, John Rushby, N. Shankar and David Stringer-Calvert, from Applied Formal Methods---FM-Trends 98, Boppard, Germany, October 1998. A brief description of PVS and a few of its applications.
Language Reference The PVS specification language is based on higher-order logic, with predicate subtypes. Some parts of the language are described in separate manuals.
Datatypes This describes the datatype mechanism in PVS, used to define recursive types, such as lists and trees.
Theory Interpretations This describes how to map uninterpreted types and constants from one theory into another. Useful for checking that your theory is consistent, and for evaluating instances of it.
PVS Semantics This gives the formal semantics for PVS.
Subtypes for Specifications: Predicate Subtyping in PVS, by John Rushby, Sam Owre, and N. Shankar, Appears in IEEE Transactions on Software Engineering, Volume 24, Number 9. September, 1998. Describes how predicate subtyping works in PVS, with many illustrative examples.
Principles and Pragmatics of Subtyping in PVS. Presented at the 14th International Workshop on Algebraic Development Techniques WADT'99, September, 1999, Toulouse, France. Further discussion of predicate subtyping in PVS.
Integration in PVS: Tables, Types, and Model Checking, by Sam Owre, John Rushby, and N. Shankar, Appears in Tools and Algorithms for the Construction and Analysis of Systems TACAS '97. Enschede, The Netherlands. April, 1997. The title says what it's about.
Prover Guide Describes the proof checker in detail, though the release notes should be consulted for newer commands as well as some new strategy writing information.
ProofLite Allows batch proving and proof scripting, enabling a semi-literate proving style, where specification and proof scripts can be kept in the same file. This is intended for non-expert users of PVS.
Real Automation in the Field Describes a built-in package of PVS strategies that supports automation of non-linear arithmetic. In particular, it includes a semi-decision procedure for the field of real numbers and a strategy for cancellation of common terms.
Manip Guide Provides an approach to tactic-based proving for improved interactive deduction. The built-in Manip package includes a set of strategies (tactics) and support functions. Although it was designed originally to reduce the tedium of low-level arithmetic manipulation, many of its features are suitable as general-purpose prover utilities. Besides strategies aimed at algebraic simplification of real-valued expressions, Manip includes term-access techniques applicable in arbitrary settings.
Writing PVS Proof Strategies (Slides) by Sam Owre and N. Shankar, from STRATA 2003, Rome, Italy, September 2003. Gives details of the PVS strategies mechanism, as well as many pragmatic examples.
Much of the PVS language is executable, and this is taken advantage of by translations to Lisp, C, and Clean. The Lisp translation was the first, and is also referred to as the Ground Evaluator. See the ground evaluator for more details.
PVSio Animation PVSio extends the ground evaluator with a predefined library of imperative programming language features such as side effects, unbounded loops, input/output operations, floating point arithmetic, exception handling, pretty printing, and parsing. The PVSio input/output library is implemented via semantic attachments.
Evaluating, Testing, and Animating PVS Specifications by Judy Crow, Sam Owre, John Rushby, N. Shankar, and Dave Stringer-Calvert, CSL Technical Report, March 30, 2001. Describes many examples using the ground evaluator.
Random Testing in PVS (Slides) by Sam Owre, from AFM 2006, Seattle, WA, August 2006. Similar to QuickCheck for Haskell, random testing in PVS allows one to look for counterexamples. This can help, for example, to refine hypotheses, before wasting time trying to prove an invalid formula.
The following are a part of PVS, but of rather specialized interest.
WS1S - PVS with Mona
In general, the specs for these tutorials are included in the latest PVS installations, under the Examples directory.
The standard introductory tutorial to PVS (WIFT) [ Examples/wift-tutorial/]: is a good place to start. It provides an introductory example and a tutorial. It is intended to provide enough information to get you started using PVS, and to help you appreciate the capabilities of the system and the purposes for which it is suitable.
A less elementary version of Ricky Butler's "Elementary Tutorial" [ Examples/elementary-tutorial/] introduces some of the more powerful strategies provided by the PVS theorem prover. It consists of two parts: the first extends a previous tutorial by Ricky Butler demonstrating how his proofs may be performed in a more automated manner; the second uses the unwinding theorem from the noninterference formulation of security to introduce theorem-proving strategies for induction. This tutorial also shows how specifications and proofs may be better presented using the LaTeX and PostScript generating facilities of PVS.
A tutorial on some advanced features of PVS [ Examples/fme96/] given at FME 96. This covers predicate subtypes and judgements in detail.
Tutorial on Specification, Proof Checking, and Model Checking for Protocols and Distributed Systems with PVS [ Examples/forte97-tutorial/] given at FORTE/PSTV 97. Analyzes a simple cache-coherence protocol using a combination of theorem proving and model checking.
PVS Tutorial, FM99 [ Examples/fm99/] given at FM 99. A simple tutorial illustrating recursion, higher-order features, and abstract datatypes of PVS.
There are many sources of PVS Examples. The PVS prelude offers foundational theories, and can easily be viewed using M-x view-prelude-theory. Another useful source of examples is in the PVS Library maintained by NASA.
Hardware Verification Using PVS [ Examples/HWVbookchap/] includes examples that appear in the chapter Hardware Verification Using PVS in the book Formal Hardware Verification Methods and Systems in Comparison, Edited by Thomas Kropf, Springer, LNCS 1287. The examples are: Arbiter, Blackjack, Detect110, Fir_filter5, Pipeline, Singlepulser, and Tamarack.
Tabular specifications and model-checking SCR transition relations [ Examples/pvs-tables/] describes PVS's capabilities for representing tabular specifications of the kind advocated by Parnas and others, and shows how PVS's Type Correctness Conditions (TCCs) are used to ensure certain well-formedness properties.
Byzantine Agreement [ Examples/byzantine/] describes the formal specification and verification of an algorithm for Interactive Consistency based on the Oral Messages algorithm for Byzantine Agreement.
Ag in PVS [ Examples/AgExample/] Ag is a specification language presented as a syntactic sugaring of the First-Order Dynamic Logic of Fork Algebras. We show how the higher-order logic theorem prover PVS can be used to build a semantic framework for reasoning about specifications written in Ag by encoding the semantics within the PVS language. We then illustrate how this semantic embedding can be used by means of a case study of a cache system specification.
