Skip to content

grantpassmore/PVS

 
 

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

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

About

The People's Verification System

Resources

License

Stars

Watchers

Forks

Packages

No packages published

Languages

  • Common Lisp 70.4%
  • C 9.5%
  • Emacs Lisp 8.3%
  • C++ 3.0%
  • Java 1.7%
  • Python 1.5%
  • Other 5.6%