A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
| Autor: | Chantal Keller, Benjamin Grégoire, Benjamin Werner, Germain Faure, Laurent Théry, Michael Armand |
|---|---|
| Přispěvatelé: | Mathematical, Reasoning and Software (MARELLE), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Types, Logic and computing (TYPICAL), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Inria Saclay - Ile de France, Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X), Jouannaud, Jean-Pierre and Shao, Zhong, ANR- 08-DEFIS-005-01,DECERT,Déduction certifiée(2008), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS), ANR-08-EMER-0005,DECERT,Déduction Certifiée(2008) |
| Jazyk: | angličtina |
| Rok vydání: | 2011 |
| Předmět: |
Soundness
Computer science Programming language business.industry [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 020207 software engineering 0102 computer and information sciences 02 engineering and technology Modular design Conjunctive normal form formula Mathematical proof computer.software_genre 01 natural sciences TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES 010201 computation theory & mathematics Satisfiability modulo theories TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS 0202 electrical engineering electronic engineering information engineering Linear arithmetic Conjunctive normal form Boolean satisfiability problem business computer |
| Zdroj: | CPP-Certified Programs and Proofs-First International Conference-2011 CPP-Certified Programs and Proofs-First International Conference-2011, Dec 2011, Kenting, Taiwan. pp.135-150, ⟨10.1007/978-3-642-25379-9_12⟩ Certified Programs and Proofs ISBN: 9783642253782 CPP |
| DOI: | 10.1007/978-3-642-25379-9_12⟩ |
| Popis: | International audience; We present a way to enjoy the power of SAT and SMT provers in Coq without compromising soundness. This requires these provers to return not only a yes/no answer, but also a proof witness that can be independently rechecked. We present such a checker, written and fully certified in Coq. It is conceived in a modular way, in order to tame the proofs' complexity and to be extendable. It can currently check witnesses from the SAT solver ZChaff 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|