ProofLite

ProofLite is a tool for non-interactive proof checking in PVS. Prooflite also enables a semi-literate proving style in PVS where specification and proof scripts reside in the same file (as it is done in Coq and other proof assistants).

ProofLite has been part of PVS since PVS 5.0 and is included in the latest release of PVS. ProofLite 6.0 provides:

• A proof script language for writing proofs in *.pvs files, e.g., prooflite_examples.pvs.
• Emacs commands for installing proof scripts in proofs and for extracting proof scripts from proofs.
• The command line utility proveit to re-prove theories in batch mode.
• The command line utility provethem to re-prove libraries (collection of theories) in batch mode.

Publications

• César Muñoz, Batch Proving and Proof Scripting in PVS, Contractor Report, NASA/CR-2007-214546, 2007. BibTex Reference.

The tag identifies links that are outside the NASA domain