search

SRI-CSL / PVS

The People's Verification System
http://pvs.csl.sri.com
GNU General Public License v2.0
139 stars 32 forks source link

readme

PVS Specification and Verification System

Build Status

PVS is a verification system: that is, a specification language integrated with support tools and a theorem prover. It is intended to capture the state-of-the-art in mechanized formal methods and to be sufficiently rugged that it can be used for significant applications. PVS is a research prototype: it evolves and improves as we develop or apply new capabilities, and as the stress of real use exposes new requirements.

For documentation and pre-built binaries, please visit http://pvs.csl.sri.com/.

Making PVS 8.0 from sources

In short:

  1. For Macs, you'll need to install xcode, in Ubuntu, apt-get install build-essential
  2. Use your favorite package manager to get SBCL and Emacs
  3. git clone https://github.com/SRI-CSL/PVS.git
  4. cd PVS
  5. Run ./configure, use your package manager if, e.g., curl is missing
  6. Run make

Notes:

  1. This works for Mac M1 natively
  2. For some reason the make on Intel Macs pauses a long time at the compile for list-decls; just be patient.
  3. There is a Dockerfile that will create a Docker image for PVS; this can be used on a Windows platform.
  4. If you're using the current version of NASA's pvslib, you will get some errors. You can temporarily use the pvs8.0 branch of https://github.com/samowre/pvslib.git, which is a fork of it upgraded to work with PVS 8.0 and SBCL.

Let us know at pvs@csl.sri.com if you have problems or suggestions.

Source layout

Files:

Directories: