These specifications and proofs in PVS support the paper,
"Model Checking Failed Conjectures in Theorem Proving: A Case Study"
Available at http://shemesh.larc.nasa.gov/fm/spider/spider_pubs.html.

Email the Corresponding Author, Lee Pike lee.s.pike@nasa.gov with any questions or inquiries.



To re-run the theory proofs, you will need to:

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 for browsing).

3. Unpack the file (tar -xzvf unified.tgz), and undump the file in PVS (M-x undump-pvs-files).  All files are imported by TOP.pvs, and therein is the conjecture generating the counter-example.

The SAL model can be found here.

Curator and Responsible NASA Official: Lee Pike
larc privacy statement
last modified: 20 July, 2004