ThePrototype Verification System (PVS) is aspecification language integrated with support tools and anautomated theorem prover, developed at the Computer Science Laboratory ofSRI International inMenlo Park, California.
PVS is based on a kernel consisting of an extension ofChurch's theory of types withdependent 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 inCommon Lisp, and is released under theGNU General Public License (GPL).
 | Thisprogramming-language-related article is astub. You can help Wikipedia byexpanding it. |
