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

• Formal methods

[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].