@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@@
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
-------
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%