These specifications and proofs in PVS support the paper, "Abstractions for Fault-Tolerant Distributed System Verification,"
to appear in Theorem Proving in Higher-Order Logics (TPHOLs), 2004.

Email the Corresponding Author, Lee Pike, at 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 as they were updated in April, 2004.

2. Download the dump file of the PVS theories (an un-tarred verion is available here for browsing).

3. Unpack the file (tar -xzvf abstractions.tgz), and undump the file in PVS (M-x undump-pvs-files).  All files are imported by top.pvs, and comments appear therein as well.

Curator and Responsible NASA Official: Lee Pike
larc privacy statement
last modified: 17 May 2004