The Prototype Verification System (PVS) is a specification language

Specification language

A specification language is a formal language used in computer science.Unlike most programming languages, which are directly executable formal languages used to implement a system, specification languages are used during systems analysis, requirements analysis and systems design.Specification...

 integrated with support tools and a theorem prover.

It was developed at the Computer Science Laboratory of SRI International

SRI International

SRI International , founded as Stanford Research Institute, is one of the world's largest contract research institutes. Based in Menlo Park, California, the trustees of Stanford University established it in 1946 as a center of innovation to support economic development in the region. It was later...

 in California

California

California is a state located on the West Coast of the United States. It is by far the most populous U.S. state, and the third-largest by land area...

. PVS is based on a kernel consisting of an extension of Church

Alonzo Church

Alonzo Church was an American mathematician and logician who made major contributions to mathematical logic and the foundations of theoretical computer science. He is best known for the lambda calculus, Church–Turing thesis, Frege–Church ontology, and the Church–Rosser theorem.-Life:Alonzo 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

Common Lisp

Common Lisp, commonly abbreviated CL, is a dialect of the Lisp programming language, published in ANSI standard document ANSI INCITS 226-1994 , . From the ANSI Common Lisp standard the Common Lisp HyperSpec has been derived for use with web browsers...

, and is released under the GNU General Public License

GNU General Public License

The GNU General Public License is the most widely used free software license, originally written by Richard Stallman for the GNU Project....

 (GPL).

External links

• PVS website at the Computer Science Laboratory, SRI.
• Summary of PVS by John Rushby
  John Rushby
  John Rushby is a British computer scientist now based in the United States.John Rushby was born and brought up in London, where he attended Dartford Grammar School. He studied at the University of Newcastle in the UK, gaining his computer science BSc there in 1971 and his PhD in 1977.From 1974 to...
  
   at the Mechanized Reasoning database of Michael Kohlhase
  Michael Kohlhase
  Dr. Michael Kohlhase is a German computer scientist and professor at Jacobs University, Bremen, Germany, where he is head of the KWARC research group at the School of Engineering and Science.-Academic Positions:Dr...
  
  and Carolyn Talcott http://www-formal.stanford.edu/clt/ARS/ars-db.html.