PV1 SMTCoqimports other solvers' proof witnesses and certificates to Coq

Plug-in for the integration of external solvers into the Coq proof assistant

Application domain/field

Type of tool

Metatool

Internals

SMTCoq is a plugin for the Coq proof assistant. It allows users to use external solvers (SAT or SMT) inside Coq. If these solvers succeed in proving a goal and return a proof witness or certificate, SMTCoq can use this to reconstruct a proof of the goal within Coq automatically. Uses CVC4, zChaff, veriT. SMTCoq is also available as an opam package.

Links

Related papers

SMTCoq: A Plug-In for Integrating SMT Solvers into Coq (CAV '17)

Last publication date

13 July 2017

ProVerB specific



ProVerB is a part of SLEBoK. Last updated: February 2023.