PVS Specification and Verification System (copy of svn repo)
Common Lisp JavaScript C Emacs Lisp HTML C++ Other
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
.travis
BDD
Examples
bin
doc
eclipse
emacs
ess
javascript
lib
pvsio-web
python
src
website
wish
.gitignore
.gitmodules
.travis.yml
INSTALL
LICENSE
Makefile.in
NOTICES
README.GUI
README.md
README.pvsio-web
config.guess
config.sub
configure.in
install-sh
proveit.in
provethem.in
pvs-config.lisp
pvs-get-patches.in
pvs-gui
pvs-tex.sub
pvs.in
pvs.sty
pvs.system
pvsio-web.in
pvsio.in

README.md

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/.

Source layout

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.