PVS: Combining specification, proof checking, and model checking

Abstract

PVS (Prototype Verification System) is an environment for constructing clear and precise specifications and for developing readable proofs that have been mechanically verified. It is designed to exploit the synergies between language and deduction, automation and interaction, and theorem proving and model checking. For example, the type system of PVS requires the use of theorem proving to establish type correctness, and conversely, type information is used extensively during a proof. Similarly, decision procedures are heavily used in order to simplify the tedious and obvious steps in a proof leaving the user to interactively supply the high-level steps in a verification. Model checking is one such decision procedure that is used to discharge temporal properties of specific finite-state systems.