Extending SMTCoq, a Certified Checker for SMT (Extended Abstract)
HaTT@IJCAR, pp. 21-29, 2016.
This extended abstract reports on current progress of SMTCoq, a communication tool between the Coq proof assistant and external SAT and SMT solvers. Based on a checker for generic first-order certificates implemented and proved correct in Coq, SMTCoq offers facilities both to check external SAT and SMT answers and to improve Coq's autom...More
PPT (Upload PPT)