SMTCoq

SMTCoq is a Coq tool that checks proof witnesses coming from external SAT and SMT solvers. It provides: It is mainly developed by Michaël Armand and Benjamin Grégoire at INRIA Sophia-Antipolis, and Chantal Keller at École Polytechnique and INRIA Saclay-Île-de-France, with some help from Germain Faure and Laurent Thery.

Sources

The source code is distributed under the terms of the CeCILL-C licence.
Download: To install it, please report to the installation instructions available in the archive. We provide a snapshot of the version of Coq required to compile it, and a snapshot of the version of veriT used for it.

Top of the page


Use

SMTCoq is designed to be used with versions of zChaff and veriT that can deliver proof witnesses. Such versions can be downloaded at: Please follow the instructions available for each solver in order to compile them in a proof production mode. In the following, we consider that the commands "veriT" or "zchaff" is in your PATH variable environment (depending on the one you want to use).

Examples

Examples are given in the file examples/Example.v available in the archive. They are meant to be easily re-usable for your own usage. Since version 1.2, extraction to OCaml is available.

Checking zChaff answers of unsatisfiability

If you want to check the result given by zChaff on an unsatisfiable dimacs file file.cnf:

Checking veriT answers of unsatisfiability

If you want to check the result given by veriT on an unsatisfiable file file.smt: The theories that are currently supported are QF_UF, QF_LIA, QF_IDL and their combinations.

zChaff as a Coq decision procedure

The zchaff tactic can be used for any goal of the form:
          forall l, b1 = b2
where l is a list of booleans (that can be concrete terms).

veriT as a Coq decision procedure

The verit tactic can be used for any goal of the form:
          forall l, b1 = b2
where l is a list of booleans. Those booleans can be any concrete terms. The theories that are currently supported are QF_UF, QF_LIA, QF_IDL and their combinations.

Extraction

The src/extraction directory contains the OCaml extracted checker, as well as additional files to make use of it. You can compile it using the given Makefile (after compiling SMTCoq): it will produce an executable in the example directory for testing. To use it, you can inspire from the file example/example.ml. Edit the first two lines of src/extraction/Makefile to compile your own files. Note that even the extracted version of SMTCoq requires both Coq and SMTCoq to be compiled (mainly since it relies on other Coq plugins).

Top of the page


Suggestions and bugs report

Do not hesitate to make any suggestion or to report bugs to Chantal Keller (remove the anti-spam at).

Top of the page


Publications about SMTCoq

  1. 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. PDF, BIBTEX

  2. 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. PDF, BIBTEX

Top of the page


Old versions

Old stable versions of SMTCoq are available (but not maintained):

Top of the page


Last update: July, 2nd 2014