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.

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:

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.