PVS Specification and Verification System


PVS is a mechanized environment for formal specification and verification. It builds on over 25 years experience at SRI in developing and using tools to support formal methods. PVS consists of a specification language, a number of predefined theories, a type checker, an interactive theorem prover that supports the use of several decision procedures and a symbolic model checker, various utilities including a code generator and a random tester, documentation, formalized libraries, and examples that illustrate different methods of using the system in several application areas. By exploiting the synergy between a highly expressive specification language and powerful automated deduction, PVS serves as a productive environment for constructing and maintaining large formalizations and proofs.


Compute Systems Invocation Version(s)
Red Hat Linux (64-bit) % /util/bin/ (default)


  1. This doesn't build properly in 64-bit RHEL:

    NOTE: The foreign functions (file_utils, BDD, and WS1S) do not currently build in 64 bit Linux - you must build these on a 32 bit machine, or modify them.


  1. Bharat Jayaraman, Instructor.


  1. http://pvs.csl.sri.com/