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

Last commit date

7 December 2021

Related papers

https://doi.org/10.1007/978-3-319-63390-9_7 (CAV '17)

Last publication date

13 July 2017

ProVerB specific

View/edit source (Markdown)



ProVerB is a part of SLEBoK. Last updated: July 2022.