@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@ Name: PVS (Prototype Verification System) Keywords: Specification/Verification Environment, Higher-order Logic, Parameterized Theories, Subtyping, Dependent Typing, Arithmetic Decision Procedures, Abstract Datatypes, Interactive Proof Checking, Model Checking. Description: Semantics: Classical higher-order logic with functions, sets, records, tuples, predicate subtypes, dependent typing, and theories with type and individual parameters. Axioms may be introduced freely; definitions (which may be recursive and include recursively-defined abstract data types and inductively defined predicates) provide conservative extension. Deductive machinery: Typechecking resolves name references, introduces user-specified type conversions, and ensures type-consistency of the specification; typechecking can generate proof obligations; subtyping judgments can be used to assert more refined typing. Proofs are developed interactively by combining high-level inference procedures such as propositional simplification, ground decision procedures, rewriting, beta-reduction, etc. User-defined proof strategies can also be invoked. BDD-based propositional simplification and mu-calculus model checking have been integrated as decision procedures. Dynamics: Theories are developed and saved as parameterized modules in (restorable) machine and human-readable forms. Proofs are saved with their theories. Libraries of specifications can be constructed and imported. Standard libraries include bit-vectors, finite sets, and a built-in "prelude" library consisting of foundational mathematical definitions and facts concerning numbers, functions, relations, induction principles, sets, and ordinal notations. Interface provided by customized GNU Emacs and Tcl/Tk displays for proof trees, commands, and theory hierarchies. System provides prettyprinting, LaTeX-printing and cross-reference generation as well as traditional deductive support. Lemmas may be used before they are proved (and can be specified and modified during a proof). "Proof-chain" analysis checks all proof obligations are discharged and identifies axiomatic and definitional foundation used. Persistence: The current context consisting of the current modules along with their status (parsed, typechecked, proved, etc.) and their proofs is saved so that a new session can be quickly restarted from the current state. Contexts can be dumped into Ascii form and mailed to other users who can undump the files to recreate the original context. Contact persons: John Rushby, N. Shankar, Sam Owre Computer Science Laboratory SRI International 333 Ravenswood Avenue Menlo Park, CA 94025 USA Email {rushby,shankar,owre}@csl.sri.com URL: http://www.csl.sri.com/pvs.html Tel: (415)859-5456/5272/5114 FAX: (415)859-2844 User group: PVS 1 was beta-released in February 1993. PVS 2 was alpha-released to users of PVS 1 in June 1995. PVS 2 will be beta-released with up-to-date documentation in late summer 1995. PVS is used by researchers in USA (SRI, Stanford, Indiana, NASA Langley, ORA Ithaca, Rockwell-Collins, etc.), Canada (UBC, York, McMaster), Denmark (Lyngby), Germany (Ulm, Kiel), Holland (Eindhoven, Utrecht), U.K. (York, Southampton), France (Paris IV, Verimag), and elsewhere. Mirror sites for PVS distribution have been established at Ulm, Germany, in ftp://ftp.informatik.uni-ulm.de/pub/KI/pvs2, and York, England, in ftp://ftp.cs.york.ac.uk/pub/pvs. To get on the PVS mailing list, send mail to pvs-request@csl.sri.com. A brief description of PVS appears in the IEEE Transactions on Software Eng. vol 21 No. 2, February, 1995 under the title "Formal verification of fault-tolerant architectures: Prolegomena to the design of PVS." Pragmatics: Strengths: Expressive specification language allows concise and natural specifications across a wide range of problem domains; Rich type system and very strict typechecking allow much of the specification to be embedded in the types with proof obligations generated automatically by the typechecker (for example, the invariant on the state of a state-machine specification induces a subtype of the states; if the operations are specified to take and return members of that subtype, then typechecking automatically generates the proof obligations necessary to show that the operations preserve the invariant). Large body of verified examples (see WWW page). Synergistic interaction between theorem proving and typechecking; Effective interactive theorem prover combining powerful arithmetic decision procedures and other "large" primitive inference steps; Ability to display "humanly readable" proofs. Weaknesses: No formal treatment of partiality though subtyping can be used to declare partial functions as total over their domain of definition. PVS sources are not freely distributed so as to preserve uniformity, but interested individuals can visit SRI to explore extensions. PVS is not an open system and presently only supports a limited range of user-supplied customizations, but there are plans for increasing the customizability. Documentation: Four volumes: language, semantics, prover, system. All except the semantics document are available for PVS 1. The complete set for PVS 2 will be available in late summer 1995. Some tutorials are available, and several papers describing applications undertaken in PVS Applications: 1. Small verifications include GCD, binomial theorem, Schroeder-Bernstein theorem, Boyer-Moore majority algorithm, ordered binary tree insertion, Wand's continuation-based program transformation, instance of Bird's fusion theorem, Rabin-Scott equivalence of DFAs, NFAs, and epsilon-NFAs, several simple pipelined and unpipelined processors, adders, and the alternating bit protocol. 2. Verification of Oral Messages algorithms for Byzantine Agreement and Interactive Consistency: both the classical (Lamport, Shostak, Pease) algorithm and the variant for hybrid fault models due to Thambidurai and Park have been formally specified and verified in PVS. Errors were discovered and corrected in the latter algorithm; a version for the Draper FTP architecture has also been verified. Also diagnosis algorithms for Byzantine fault-tolerant architectures. 3. Axiomatization of a Unity-like system for reasoning about real-time computations, and formal specification and verification of Fischer's mutual exclusion algorithm and a generalized railroad-crossing example. 4. The Collins AAMP5 avionics processor. The microarchitecture and most of the instruction set architecture (108 out of 209 instructions) of this complex processor (500,000 transistors, three-stage pipeline, stack architecture, autonomous subunits) were formally specified in PVS and the microcode of 11 representative instructions were formally verified, leading to the discovery of both real and seeded errors. 5. Verification of an N-process generalization of Peterson's mutual exclusion algorithm. The proof is by induction on the number of processes where the induction step uses the induction hypothesis to abstract the n-process system to a single finite-state process, and model checking is used to verify the n+1-process algorithm. 6. Specification of the IEEE-854 Floating Point standard (by Paul Miner). 7. Various examples using Hoare logic with real-time extensions (by Jozef Hooman and Jan Vitt). Extensions/enhancements: Plan to provide quotient types, mutually recursive datateyps, and support for verification of the "implements" relation between specifications. Also more support for early exploration and validation of specifications by direct execution and state exploration. Provision of more "open" system architecture. Resource requirements: implementation language: Common Lisp/CLOS; requires native CLOS for good performance; runs well under Lucid and Allegro Lisp on Sun Sparc workstations under SunOS 4.1 and Solaris; unacceptable performance under AKCL; Lucid Lisp version requires license, Allegro Lisp version does not. Environment support required: uses Gnu Emacs as its interface; typeset specifications require LaTeX; graphical displays require X11 and Tcl/Tk. Needs at least 32Mbytes of real memory, 50+ Mbytes of swap space, 25 MBytes of disk space. Where-to-get-it: ftp: ftp.csl.sri.com:/pub/pvs/pvs2 http://www.csl.sri.com/pvs.html John Rushby, Aug 1, 1995 ------- %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%