NATIONAL INSTITUTE OF AEROSPACE

Contact Us

Colin Britcher, Ph.D.
Director of Graduate Education
757.325.6730
colin.britcher@nianet.org  

Mary Catherine Bunde, M.Ed.
Senior Education Administrator
757.325.6731
mary.bunde@nianet.org

8.14.15 Gilbert

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.

BUSINESS WITH NIA

Headquarters

100 Exploration Way
Hampton, VA 23666
(757)325-6700
www.nianet.org