Extending SMTCoq, a Certified Checker for SMT (Extended Abstract)

Chantal Keller
Chantal Keller
Andrew J. Reynolds
Andrew J. Reynolds

HaTT@IJCAR, pp. 21-29, 2016.

Cited by: 0|Bibtex|Views6|Links
EI

Abstract:

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

Code:

Data:

Your rating :
0

 

Tags
Comments