Verifying SAT and SMT in Coq for a fully automated decision procedure

Mickaël Armand 1 Germain Faure 2 Benjamin Grégoire 1 Chantal Keller 2 Laurent Théry 1 Benjamin Wener 2, 3
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
2 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, X - École polytechnique, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : Enjoying the power of SAT and SMT solvers in the Coq proof as- sistant without compromising soundness requires more than a yes/no answer from them. SAT and SMT solvers should also return a proof witness that can be checked by an external tool. We propose a fully certified checker for such witnesses written in Coq. It can currently check witnesses from the SAT solvers ZChaff and MiniSat and from the SMT solver VeriT. Experiments highlight the efficiency of this checker. On top of it, new reflexive Coq tactics have been built that can decide a subset of Coq's logic by calling external provers and carefully checking their answers.
Type de document :
Communication dans un congrès
PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories, Aug 2011, Wroclaw, Poland. 2011
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00614041
Contributeur : Assia Mahboubi <>
Soumis le : lundi 8 août 2011 - 21:44:52
Dernière modification le : jeudi 10 mai 2018 - 02:06:41
Document(s) archivé(s) le : mercredi 9 novembre 2011 - 02:26:06

Fichier

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

Identifiants

  • HAL Id : inria-00614041, version 1

Citation

Mickaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, et al.. Verifying SAT and SMT in Coq for a fully automated decision procedure. PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories, Aug 2011, Wroclaw, Poland. 2011. 〈inria-00614041〉

Partager

Métriques

Consultations de la notice

420

Téléchargements de fichiers

552