A framework for proof certificates in finite state exploration

Quentin Heath 1 Dale Miller 1
1 PARSIFAL - Proof search and reasoning with logic specifications
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR7161
Abstract : Model checkers use automated state exploration in order to prove various properties such as reach-ability, non-reachability, and bisimulation over state transition systems. While model checkers have proved valuable for locating errors in computer models and specifications, they can also be used to prove properties that might be consumed by other computational logic systems, such as theorem provers. In such a situation, a prover must be able to trust that the model checker is correct. Instead of attempting to prove the correctness of a model checker, we ask that it outputs its " proof evidence " as a formally defined document—a proof certificate—and that this document is checked by a trusted proof checker. We describe a framework for defining and checking proof certificates for a range of model checking problems. The core of this framework is a (focused) proof system that is augmented with premises that involve " clerk and expert " predicates. This framework is designed so that soundness can be guaranteed independently of any concerns for the correctness of the clerk and expert specifications. To illustrate the flexibility of this framework, we define and formally check proof certificates for reachability and non-reachability in graphs, as well as bisimulation and non-bisimulation for labeled transition systems. Finally, we describe briefly a reference checker that we have implemented for this framework.
Type de document :
Communication dans un congrès
Proceedings of the Fourth Workshop on Proof eXchange for Theorem Proving, Aug 2015, Berlin, Germany. 2015, 〈10.4204/EPTCS.186.4〉
Liste complète des métadonnées

Littérature citée [19 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01240172
Contributeur : Dale Miller <>
Soumis le : mardi 8 décembre 2015 - 17:27:36
Dernière modification le : jeudi 10 mai 2018 - 02:06:56
Document(s) archivé(s) le : samedi 29 avril 2017 - 10:15:18

Fichier

pxtp2015.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Quentin Heath, Dale Miller. A framework for proof certificates in finite state exploration. Proceedings of the Fourth Workshop on Proof eXchange for Theorem Proving, Aug 2015, Berlin, Germany. 2015, 〈10.4204/EPTCS.186.4〉. 〈hal-01240172〉

Partager

Métriques

Consultations de la notice

334

Téléchargements de fichiers

51