SMTCoq: A Plug-In for Integrating SMT Solvers into Coq
CAV, pp. 126-133, 2017.
This paper describes SMTCoq, a plug-in for the integration of external solvers into the Coq proof assistant. Based on a checker for generic first-order proof certificates fully implemented and proved correct in Coq, SMTCoq offers facilities to check answers from external SAT and SMT solvers and to increase Coq’s automation using such solv...More
PPT (Upload PPT)