View on GitHub

SMTCoq

Download this project as a .zip file Download this project as a tar.gz file

Presentation

SMTCoq is a Coq plugin that checks proof witnesses coming from external SAT and SMT solvers. It provides:

Installation and use

SMTCoq is freely available as an opam package and on GitHub.

To use the CVC4 SMT solver, you must download the lfsc branch.

New:

These three features will be merged in a realease to come in November 2018.

SMTCoq is distributed under the CeCILL-C license.

People

Current team

Past contributors

Publications

Reference

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.

Other publications

  1. 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.
  2. 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.
  3. 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.