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.

Theorem Provers

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