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.

PropertyValue
dbpprop:abstract
  • 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).
  • PVS (Prototype Verification System) est un assistant de preuve développé par le laboratoire d'informatique de SRI International.
dbpprop:hasPhotoCollection
dbpprop:reference
rdf:type
rdfs:comment
  • 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.
  • PVS (Prototype Verification System) est un assistant de preuve développé par le laboratoire d'informatique de SRI International.
rdfs:label
  • Prototype Verification System
  • Prototype Verification System
owl:sameAs
skos:subject
foaf:page
is dbpprop:redirect of
is owl:sameAs of