PROOF CERTIFICATES IN PVS
Frederic Gibert, Ecole de Ponts Paris Tech, France
August 14, 2015, 11:00 am, NASA Langley, Bldg 1220, Rm 110
Abstract:
A possible way to reach higher safety guarantees with PVS is to allow independent proof systems to rerun and verify PVS results. This can be done by instrumenting PVS to output proof certificates. Unlike the existent notion of PVS proofs, which allows PVS to check its own results efficiently, these certificates must be expressed in a sufficiently explicit and generic language to be understood by third party systems. The purpose of the current work is to instrument the PVS proof engine to emit such certificates step by step during the proof process. The very first steps towards this goal are presented. In particular, we show how proof certificates are formalized in a sequent calculus proof language, and how PVS is being instrumented to output such proof certificates
Bio:
Frederic is a PhD student at Ecole de Ponts Paris Tech in France.