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
SMTCoq is distributed under the CeCILL-C license.
- Clark Barrett (Stanford University)
- Valentin Blot (Université Paris-Sud)
- Burak Ekici (The University of Iowa)
- 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.