PVS Examples

PVS 6.0

PVS 3.1

PVS 2.4 and 2.3

The theories below may not be compatible with PVS2.2 (some use the new syntax and judgements). The proofs have been done using the old decision procedures but, with a few exceptions, everything also works with the new ones. When available, the 2.4 versions contain minor modifications.

PVS 2.2

Most of the things below are (gzipped) dump files produced with PVS version 2.414 or older.
The proofs should work with newer versions but some adjustments may be necessary.