NASA logo

+ Contact NASA



  • + HOME
  • + WELCOME
  • + QUICK PAGE
  • + PHILOSOPHY
  • + TEAM
  • + RESEARCH
  • + LINKS

  • 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. The current version of ProofLite is 6.0 and is included in PVS 6.0*. ProofLite 6.0 provides:

    Publications

    The tag [*] identifies links that are outside the NASA domain