Prototype Verification System
From Wikipedia, the free encyclopedia
PVS, or the Prototype Verification System, is a specification language integrated with support tools and a theorem prover, developed at the Computer Science Laboratory of SRI International, California, USA. It is based on a kernel consisting of an extension of Church's theory of types with dependent types. The system is implemented in Common LISP.
[edit] Reference
- Owre, Shankar, and Rushby, 1992. PVS: A Prototype Verification System. Published in the CADE 11 conference proceedings.
[edit] See also
[edit] External links
- PVS website at the Computer Science Laboratory, SRI.
- Summary of PVS by John Rushby at the Mechanized Reasoning database of Michael Kohlhase and Carolyn Talcott [1].
