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 firstname.lastname@example.org with any
questions or inquiries.
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 as they were updated in April, 2004.
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 undump-pvs-files
All files are imported by top.pvs, and comments appear therein as
Curator and Responsible NASA Official: Lee Pike
larc privacy statement
last modified: 17 May 2004