SMTCoq is a Coq plugin that checks proof witnesses coming from external SAT and SMT solvers. It provides:
- a certified checker for proof witnesses coming from the SAT solver ZChaff and the SMT solvers veriT and CVC4. This checker increases the confidence in these tools by checking their answers a posteriori and allows to import new theroems proved by these solvers in Coq;
- decision procedures through new tactics that discharge some Coq goals to ZChaff, veriT and CVC4.
Installation and use
To use the CVC4 SMT solver, you must download the lfsc branch.
verittactic now has support for quantifiers: see the end of this file for examples
N_convertnow allow to reason about other types of integers: see also the end of this file for examples
These three features will be merged in a realease to come in December 2018.
SMTCoq is distributed under the CeCILL-C license.
- Clark Barrett (Stanford University)
- Valentin Blot (Université Paris-Sud, Université Paris-Diderot)
- Amina Bousalem (Université Paris-Sud)
- Burak Ekici (The University of Iowa)
- Quentin Garchery (Université Paris-Sud, Inria)
- Benjamin Grégoire (Inria Sophia Antipolis)
- Guy Katz (Stanford University)
- Chantal Keller (Université Paris-Sud)
- Alain Mebsout (OcamlPro)
- Andrew Reynolds (The University of Iowa)
- Laurent Théry (Inria Sophia Antipolis)
- Cesare Tinelli (The University of Iowa)
- Mikaël Armand (Inria Sophia Antipolis)
- Germain Faure (Inria Saclay)
- Tianyi Liang (The University of Iowa)
- Benjamin Werner (École polytechnique)
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, Armand, Michaël; Faure, Germain; Grégoire, Benjamin; Keller, Chantal; Thery, Laurent; Werner, Benjamin, CPP - Certified Programs and Proofs - First International Conference - 2011.
- SMTCoq: A plug-in for integrating SMT solvers into Coq (Tool Paper), Ekici, Burak; Mebsout, Alain; Tinelli, Cesare; Keller, Chantal; Katz, Guy; Reynolds, Andrew; Barrett, Clark, CAV - International Conference on Computer Aided Verification - 2017.
- Extending SMTCoq, a Certified Checker for SMT (Extended Abstract), Ekici, Burak; Katz, Guy; Keller, Chantal; Mebsout, Alain; Reynolds, Andrew; Tinelli, Cesare, HaTT - on Hammers for Type Theories - First International Workshop - 2016.
- Verifying SAT and SMT in Coq for a fully automated decision procedure, Armand, Mickaël; Faure, Germain; Grégoire, Benjamin; Keller, Chantal; Théry, Laurent; Wener, Benjamin, PSATTT - International Workshop on Proof-Search in Axiomatic Theories and Type Theories - 2011.