Journal article
Extending SMTCoq, a Certified Checker for SMT (Extended Abstract)
Electronic proceedings in theoretical computer science, Vol.210(Proc. HaTT 2016), pp.21-29
06/19/2016
DOI: 10.4204/EPTCS.210.5
Abstract
EPTCS 210, 2016, pp. 21-29 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 automation using such solvers, in a safe way. Currently
supporting the SAT solver zChaff, and the SMT solver veriT for the combination
of the theories of congruence closure and linear integer arithmetic, SMTCoq is
meant to be extendable with a reasonable amount of effort: we present work in
progress to support the SMT solver CVC4 and the theory of bit vectors.
Details
- Title: Subtitle
- Extending SMTCoq, a Certified Checker for SMT (Extended Abstract)
- Creators
- Burak Ekici - The University of IowaGuy Katz - New York UniversityChantal Keller - LRI, Univ. Paris-SudAlain Mebsout - The University of IowaAndrew J Reynolds - The University of IowaCesare Tinelli - The University of Iowa
- Resource Type
- Journal article
- Publication Details
- Electronic proceedings in theoretical computer science, Vol.210(Proc. HaTT 2016), pp.21-29
- DOI
- 10.4204/EPTCS.210.5
- ISSN
- 2075-2180
- eISSN
- 2075-2180
- Language
- English
- Date published
- 06/19/2016
- Academic Unit
- Computer Science
- Record Identifier
- 9984002434702771
Metrics
18 Record Views