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 theorem prover. The latest 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 licence.

Previous versions are available free-of-charge for non-commercial use only, which technically makes them non-free. The web site for PVS explains the capabilities and licensing terms for the system.

Theorem Provers

CLiki pages can be edited by anyone at any time. Imagine a fearsomely comprehensive disclaimer of liability. Now fear, comprehensively