Skip to Main content Skip to Navigation
Conference papers

Proof certificates in PVS

Frédéric Gilbert 1, 2
1 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
Inria Saclay - Ile de France, LSV - Laboratoire Spécification et Vérification [Cachan]
2 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
Abstract : The purpose of this work is to allow the proof system PVS to export proof certificates that can be checked externally. This is done through the instrumentation of PVS to record detailed proofs step by step during the proof search process. At the current stage of this work, proofs can be built for any PVS theory. However, some reasoning steps rely on unverified assumptions. For a restricted fragment of PVS, the proofs are exported to the universal proof checker Dedukti, and the un-verified assumptions are proved externally using the automated theorem prover MetiTarski.
Complete list of metadatas

Cited literature [6 references]  Display  Hide  Download
Contributor : Frédéric Gilbert <>
Submitted on : Saturday, December 30, 2017 - 11:48:17 AM
Last modification on : Tuesday, July 7, 2020 - 11:52:47 AM


Files produced by the author(s)



Frédéric Gilbert. Proof certificates in PVS. ITP 2017 - 8th International Conference on Interactive Theorem Proving, Sep 2017, Brasilia, Brazil. pp.262-268, ⟨10.1007/978-3-319-66107-0_17⟩. ⟨hal-01673517⟩



Record views


Files downloads