Prototype Verification System
- Prototype Verification System
PVS, or the Prototype Verification System, is a specification language integrated 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).
References
* Owre, Shankar, and Rushby, 1992. "PVS: A Prototype Verification System". Published in the "CADE 11" conference proceedings.
ee also
*Formal methods
External links
* [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 Rushby at the "Mechanized Reasoning" database of Michael Kohlhase and Carolyn Talcott [http://www-formal.stanford.edu/clt/ARS/ars-db.html] .
Wikimedia Foundation.
2010.
Look at other dictionaries:
Prototype Verification System — Pour les articles homonymes, voir PVS. PVS (Prototype Verification System) est un assistant de preuve développé par le laboratoire d informatique de SRI International. Portail de l’inf … Wikipédia en Français
Prototype — A prototype is an original type, form, or instance of something serving as a typical example, basis, or standard for other things of the same category. The word derives from the Greek πρωτότυπον ( prototypon ), archetype, original , neutral of… … Wikipedia
Type system — Type systems Type safety Inferred vs. Manifest Dynamic vs. Static Strong vs. Weak Nominal vs. Structural Dependent typing Duck typing Latent typing Linear typing Uniqueness typing … Wikipedia
Cover system — For the real world military tactic of avoiding hostile gunfire, see Cover (military) … Wikipedia
Common Lisp — Paradigm(s) Multi paradigm: procedural, functional, object oriented, meta, reflective, generic Appeared in 1984, 1994 for ANSI Common Lisp Developer ANSI X3J13 committee Typing discipline … Wikipedia
Methode formelle (informatique) — Méthode formelle (informatique) Pour les articles homonymes, voir Méthode. En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l aide de logique mathématique, sur des programmes informatiques ou… … Wikipédia en Français
Méthode formelle — (informatique) Pour les articles homonymes, voir Méthode. En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l aide de logique mathématique, sur des programmes informatiques ou des matériels… … Wikipédia en Français
Méthode formelle (informatique) — Pour les articles homonymes, voir Méthode. En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l aide de logique mathématique, sur des programmes informatiques ou des matériels électroniques, afin … Wikipédia en Français
Méthodes formelles — Méthode formelle (informatique) Pour les articles homonymes, voir Méthode. En informatique, les méthodes formelles sont des techniques permettant de raisonner rigoureusement, à l aide de logique mathématique, sur des programmes informatiques ou… … Wikipédia en Français
Interactive theorem proving — is the field of computer science and mathematical logic concerned with tools to develop formal proofs by man machine collaboration. This involves some sort of proof assistant: an interactive proof editor, or other interface, with which a human… … Wikipedia
