SMTCoq: A Plug-In for Integrating SMT Solvers into Coq

CAV, pp. 126-133, 2017.

Cited by: 40|Bibtex|Views20|Links
EI

Abstract:

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

Code:

Data:

Your rating :
0

 

Tags
Comments