PVS (Prototype Verification System) is a specification language and theorem prover for validating specifications. PVS helps engineers to design coherent specifications, and to predict the behaviour of systems satisfying the specifications — before implementing them. PVS provides interactive assistance to prove theorems that validate the specifications/models. PVS has been used by OPG to certify nuclear reactors, by NASA for space/avionic systems, and in a large number of other mission critical applications. PVS is both a language and an inference system. The language is a typed higher order logic, featuring undecidable type checking. You cannot write code (such as Java, Ruby or Haskell). You can only write mathematics. It thus forces one to write specifications of systems (i.e. what systems do free of implementation detail) and not how they do it. Furthermore, PVS can so some automatic syntax, typing and other checks that helps ensure that specifications are meaningful. PVS can then be used to validate the specifications. PVS was featured in the movie The Martian.

• SRI PVS Site
• SRI Documentation
• NASA PVS site
• This site: pvs.eecs.yorku.ca. EECS Wiki] ===== Current Components ===== * PVS version 6.0 * Nasalib 6.0.9 * Nasalib come with a batch ''proveit'' facility, ''hypatheon'' (for browsing the NASA libraries), and [[http://shemesh.larc.nasa.gov/people/cam/PVSio/|PVSio (for ground evaluation).