What is PVS?

PVS is a mechanized environment for formal specification and verification. It builds on over 25 years experience at SRI in developing and using tools to support formal methods. PVS consists of a specification language, a number of predefined theories, a type checker, an interactive theorem prover that supports the use of several decision procedures and a symbolic model checker, various utilities including a code generator and a random tester, documentation, formalized libraries, and examples that illustrate different methods of using the system in several application areas. By exploiting the synergy between a highly expressive specification language and powerful automated deduction, PVS serves as a productive environment for constructing and maintaining large formalizations and proofs.

How to get PVS?

PVS 6.0 is the current stable version of the tool. You can freely download PVS, but you must must read and accept the click-through license that comes up when you choose the download. If you are a commercial entity and you don't have a PVS license, please contact us at pvs-licensing@csl.sri.com

Manuals

To effectively use PVS, you should consult at least the System Guide, the Language Reference, and the Prover Guide. Additional useful documents include the PVSio animation environment, and the PVSio-web prototyping tool. Tutorials, examples, and case studies are also available from our Resources page.

Modeling with PVS Higher Order Logic

The specification language of PVS is based on classical, typed higher-order logic. The base types include uninterpreted types that may be introduced by the user, and built-in types such as the booleans, integers, reals, and the ordinals up to epsilon_0; the type-constructors include functions, sets, tuples, records, enumerations, and inductively-defined abstract data types, such as lists and binary trees, and coinductively-defined abstract data types such as streams. Predicate subtypes and dependent types can be used to introduce constraints, such as the type of prime numbers or order-preserving maps. These constrained types may incur proof obligations (called type-correctness conditions or TCCs) during typechecking, but greatly increase the expressiveness and naturalness of specifications. In practice, most of the obligations are discharged automatically by the theorem prover. PVS specifications are organized into parameterized theories that may contain assumptions, definitions, axioms, and theorems. Parameters can include constants, types, and theory instances. Theory interpretations are used to instantiate the declared types and constants in a theory with definitions. Theory interpretations can be used for exhibiting models for an axiomatic theory and to refine a abstract theory in terms of a concrete one. Definitions are guaranteed to be conservative extensions; to ensure this, recursive function definitions generate termination proof obligations. Inductively-defined relations are also supported. PVS expressions provide the usual arithmetic and logical operators, function application, lambda abstraction, and quantifiers, within a natural syntax. Names may be freely overloaded, including those of the built-in operators such as AND and +. Tabular specifications of the kind advocated by Parnas are supported, with automated checks for disjointness and coverage of conditions. An extensive prelude of built-in theories provides hundreds of useful definitions and lemmas; user-contributed libraries provide many more.

Verification with the PVS Theorem Prover

The PVS theorem prover provides a collection of powerful primitive inference procedures that are applied interactively under user guidance within a sequent calculus framework. The primitive inferences include propositional and quantifier rules, induction, rewriting, simplification using decision procedures for equality and linear arithmetic, data and predicate abstraction, and symbolic model checking. The implementations of these primitive inferences are optimised for large proofs: for example, propositional simplification uses BDDs, and auto-rewrites are cached for efficiency. User-defined procedures can combine these primitive inferences to yield higher-level proof strategies. There is a synergistic interaction between the PVS language features and the prover so that the type information associated with a term is exploited by the inference mechanisms, and conversely, the automation in the prover is helpful in automatically discharging TCCs. Proofs yield scripts that can be edited, attached to additional formulas, and rerun. This allows many similar theorems to be proved efficiently, permits proofs to be adjusted economically to follow changes in requirements or design, and encourages the development of readable proofs.

PVS includes a BDD-based decision procedure for the relational mu-calculus and thereby provides an experimental integration between theorem proving and CTL model checking. PVS has recently been extended to use the Yices SMT solver as an endgame prover and an infinite-state bounded model checker, the PVSio framework for evaluating ground PVS expressions, and a random testing capability that can be used during proofs.

PVSio Animation Environment

PVSio is the animation environment of PVS. It is built on top of the PVS ground evaluator, which generates Common Lisp code from PVS functional specifications to evaluate ground expressions on top of the PVS underlying Common Lisp environment. PVSio provides 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 current version of PVSio provides:

  1. A standard library of semantic attachments.
  2. A high level interface for writing user-defined semantic attachments.
  3. A simpler Emacs interface and a stand alone Emacs-free interface to the ground evaluator.
  4. The proof commands eval-expr and eval-formula that safely integrate the ground evaluator into the PVS theorem prover. These proof rules use the efficient Common Lisp code generated by the ground evaluator to simplify ground expressions in sequent formulas.
PVSio-web Prototyping Environment

PVSio-web is a graphical environment that transforms the animation capabilities of the standard PVS theorem proving system with a sophisticated graphical front-end allowing interactive (human-computer) systems modelling and prototyping. Using PVSio-web, one can generate and evaluate realistic interactive prototypes from formal models. PVSio-web has been successfully used over the last two years for analysing commercial medical devices, and has been used to create training material for device developers and device users. For safety-critical medical device design, PVSio-web has been used with formal methods experts and with non-technical end users, including doctors and nurses.