PVS‎ > ‎



PBS library dumps and corresponding proof status, mainly 5.0 and ENSEIRB-MATMECA.
This Google drive folder contains PVS library dumps that are usually compatible with PVS 5.0, even if they were produced with earlier versions, such as PVS 2.4.

Each dump often comes with the corresponding Proof Status (usually with everything proved complete).

Dumps are not inclusive: each dumped library may rely upon one or more libraries represented by separate dumps; the used libraries should of course be reconstructed first.

Unless otherwise specified, these libraries have been developed at ENSEIRB-MATMECA or LaBRI.

The source of this Google Drive folder is thus ~gloess/pvsdir/, where all the libraries are stored, mixed with .pvs or .prf files.

Students: note that some of these dumps are solutions to exercises: you should not look at them too early!