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/.
In short: 0. For Macs, you'll need to install xcode, in Ubuntu, apt-get install build-essential
- Use your favorite package manager to get SBCL and Emacs
- git clone https://github.com/SRI-CSL/PVS.git
- cd PVS
- Run ./configure, use your package manager if, e.g., curl is missing
- Run make
Notes:
- This works for Mac M1 natively
- For some reason the make on Intel Macs pauses a long time at the compile for list-decls; just be patient.
- There is a Dockerfile that will create a Docker image for PVS; this can be used on a Windows platform.
- 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 [email protected] if you have problems or suggestions.
Files:
- README - this file
- pvs - the shell script for invoking pvs
- pvsio-web - the shell script for invoking the pvsio-web prototyping tool
- pvs.sty - the style file supporting LaTeX output
- pvs-tex.sub - the default substitution file for generating LaTeX
Directories:
- Examples - some simple example specifications
- emacs - Emacs files.
- wish - Tcl/Tk files
- bin - shell scripts and executables
- lib - prelude, help files, and libraries
- pvsio-web - PVSio-web prototyping tool and example prototypes
- javascript - experimental javascript front-ends for PVS. See javascript/README.md for more info on how to run the tools.