Introduction

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.

Usage

Notes

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.

People

1. Bharat Jayaraman, Instructor.

References

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