Modular SMT Proofs for Fast Reflexive Checking inside Coq

Frédéric Besson 1 Pierre-Emmanuel Cornilleau 1 David Pichardie 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : We present a new methodology for exchanging unsatisfia- bility proofs between an untrusted SMT solver and a sceptical proof assistant with computation capabilities like Coq. We advocate modular SMT proofs that separate boolean reasoning and theory reasoning; and structure the communication between theories using Nelson-Oppen combination scheme. We present the design and implementation of a Coq reflexive verifier that is modular and allows for fine-tuned theory-specific verifiers. The current verifier is able to verify proofs for quantifier-free formulae mixing linear arithmetic and uninterpreted functions. Our proof generation scheme benefits from the efficiency of state-of-the-art SMT solvers while being independent from a specific SMT solver proof format. Our only requirement for the SMT solver is the ability to extract unsat cores and generate boolean models. In practice, unsat cores are relatively small and their proof is obtained with a modest overhead by our proof-producing prover. We present experiments assessing the feasibility of the approach for benchmarks obtained from the SMT competition.
Type de document :
Communication dans un congrès
First International Conference on Certified Programs and Proofs, 2011, Kenting, Taiwan. 2011
Liste complète des métadonnées

https://hal.inria.fr/hal-00646960
Contributeur : Frédéric Besson <>
Soumis le : jeudi 1 décembre 2011 - 09:35:34
Dernière modification le : vendredi 16 novembre 2018 - 01:40:09
Document(s) archivé(s) le : lundi 5 décembre 2016 - 07:40:29

Fichier

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

Identifiants

  • HAL Id : hal-00646960, version 1

Citation

Frédéric Besson, Pierre-Emmanuel Cornilleau, David Pichardie. Modular SMT Proofs for Fast Reflexive Checking inside Coq. First International Conference on Certified Programs and Proofs, 2011, Kenting, Taiwan. 2011. 〈hal-00646960〉

Partager

Métriques

Consultations de la notice

930

Téléchargements de fichiers

146