An Entity of Type: language, from Named Graph: http://dbpedia.org, within Data Space: dbpedia.org

The Prototype Verification System (PVS) is a specification language integrated with support tools and an automated theorem prover, developed at the Computer Science Laboratory of SRI International in Menlo Park, California. The system is implemented in Common Lisp, and is released under the GNU General Public License (GPL).

Property Value
dbo:abstract
  • PVS (Prototype Verification System) est un assistant de preuve développé par le laboratoire d’informatique de SRI International. (fr)
  • The Prototype Verification System (PVS) is a specification language integrated with support tools and an automated theorem prover, developed at the Computer Science Laboratory of SRI International in Menlo Park, California. 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). (en)
dbo:thumbnail
dbo:wikiPageExternalLink
dbo:wikiPageID
  • 1848947 (xsd:integer)
dbo:wikiPageLength
  • 2032 (xsd:nonNegativeInteger)
dbo:wikiPageRevisionID
  • 985018653 (xsd:integer)
dbo:wikiPageWikiLink
dbp:wikiPageUsesTemplate
dcterms:subject
rdf:type
rdfs:comment
  • PVS (Prototype Verification System) est un assistant de preuve développé par le laboratoire d’informatique de SRI International. (fr)
  • The Prototype Verification System (PVS) is a specification language integrated with support tools and an automated theorem prover, developed at the Computer Science Laboratory of SRI International in Menlo Park, California. The system is implemented in Common Lisp, and is released under the GNU General Public License (GPL). (en)
rdfs:label
  • Prototype Verification System (fr)
  • Prototype Verification System (en)
owl:sameAs
prov:wasDerivedFrom
foaf:depiction
foaf:isPrimaryTopicOf
is dbo:knownFor of
is dbo:wikiPageDisambiguates of
is dbo:wikiPageRedirects of
is dbo:wikiPageWikiLink of
is dbp:knownFor of
is foaf:primaryTopic of
Powered by OpenLink Virtuoso    This material is Open Knowledge     W3C Semantic Web Technology     This material is Open Knowledge    Valid XHTML + RDFa
This content was extracted from Wikipedia and is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License