- Prototype Verification System
PVS, or the Prototype Verification System, is a
specification languageintegrated with support tools and a theorem prover.
It was developed at the Computer Science Laboratory of
SRI International, California, USA. PVS is based on a kernel consisting of an extension of Church's theory of types with dependent types, and is fundamentally a 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. Type-constructors include functions, sets, tuples, records, enumerations, and abstract data types. Predicate subtypes and dependent types can be used to introduce constraints; these constrained types may incur proof obligations (called type-correctness conditions or TCCs) during typechecking. PVS specifications are organized into parameterized theories.
The system is implemented in
Common Lisp, and is released under the GNU General Public License(GPL).
* Owre, Shankar, and Rushby,
1992. "PVS: A Prototype Verification System". Published in the "CADE 11" conference proceedings.
* [http://pvs.csl.sri.com/ PVS website] at the Computer Science Laboratory, SRI.
* [http://www-formal.stanford.edu/clt/ARS/Entries/pvs Summary of PVS] by
John Rushbyat the "Mechanized Reasoning" database of Michael Kohlhaseand Carolyn Talcott [http://www-formal.stanford.edu/clt/ARS/ars-db.html] .
Wikimedia Foundation. 2010.