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.
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.
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.
PVS uses Gnu or X Emacs to provide an integrated interface to its specification language and prover. Commands can be selected either by pull-down menus or by extended Emacs commands. Extensive help, status-reporting and browsing tools are available, as well as the ability to generate typeset specifications (in user-defined notation) using LaTeX. Proof trees and theory hierarchies can be displayed graphically using Tcl/Tk.
Typical applications of PVS include the formalization of mathematical concepts and proofs in areas such as analysis, graph theory, and number theory, the embedding of formalisms such as I/O automata and modal and temporal logics, the verification of hardware, sequential and distributed algorithms, and as a back-end verification tool for computer algebra and code verification systems. Several examples are described in papers listed on the documentation page.
PVS has been installed at hundreds of sites in North America, Europe, and Asia; current work is developing PVS methodologies for hghly automated hardware verification (including integration with model checkers), and for concurrent and real-time systems.
For further information on PVS, start at the top level of the PVS Web Site, the PVS Wiki, or send mail to us at pvs-request@csl.sri.com.