Book chapter
SMTCoq: A Plug-In for Integrating SMT Solvers into Coq
Computer Aided Verification, pp.126-133
Lecture Notes in Computer Science, Springer International Publishing
07/13/2017
DOI: 10.1007/978-3-319-63390-9_7
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 solvers, all in a safe way. The current version supports proof certificates produced by the SAT solver ZChaff, for propositional logic, and the SMT solvers veriT and CVC4, for the quantifier-free fragment of the combined theory of fixed-size bit vectors, functional arrays with extensionality, linear integer arithmetic, and uninterpreted function symbols.
Details
- Title: Subtitle
- SMTCoq: A Plug-In for Integrating SMT Solvers into Coq
- Creators
- Burak Ekici - The University of Iowa, Iowa City, USAAlain Mebsout - The University of Iowa, Iowa City, USACesare Tinelli - The University of Iowa, Iowa City, USAChantal Keller - LRI, Univ. Paris-Sud, CNRS, Université Paris-Saclay, Orsay, FranceGuy Katz - Stanford University, Stanford, USAAndrew Reynolds - The University of Iowa, Iowa City, USAClark Barrett - Stanford University, Stanford, USA
- Resource Type
- Book chapter
- Publication Details
- Computer Aided Verification, pp.126-133
- Publisher
- Springer International Publishing; Cham
- Series
- Lecture Notes in Computer Science
- DOI
- 10.1007/978-3-319-63390-9_7
- eISSN
- 1611-3349
- ISSN
- 0302-9743
- Language
- English
- Date published
- 07/13/2017
- Academic Unit
- Computer Science
- Record Identifier
- 9984002307002771
Metrics
16 Record Views