PVS Specification and Verification System

The PVS Specification and Verification System is a verification system: that is, a specification language integrated with support tools and a highly automated and higher order theorem prover.

• From version 5, PVS also supports SBCL
• From version 4.1, PVS works best with Allegro but it also works with CMUCL.
• Version 4.0 works best with ACL 8.0 (should work with version >= 6.2). CMUCL 19c is also supported.

As of version 4.0 (november 2006) PVS is now distributed under the terms of the GPL license.

Repository: https://github.com/SRI-CSL/PVS

Theorem Provers

Account name Password

register