To re-run the theory proofs, you will
1. Download the NASA
Langley Research Center PVS Libraries for PVS 3.1 and the PVS
strategies Manip and Field
(all are obtainable in one tar file on
the download page, and instructions are there, too). If you
already have downloaded the libraries,
make sure they are up-to-date.
2. Download the dump file of the PVS theories
(an un-tarred verion is available here
3. Unpack the file (tar -xzvf
), and undump the file in PVS (M-x
All files are imported by TOP.pvs, and therein is the conjecture
generating the counter-example.
The SAL model can be found here