SMTCoq: A Plug-In for Integrating SMT Solvers into Coq
In: Computer Aided Verification ISBN: 9783319633893 CAV (2) Computer Aided Verification-29th International Conference Computer Aided Verification-29th International Conference, Jul 2017, Heidelberg, Germany; (2017)
Online
unknown
Zugriff:
International audience; 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.
| Titel: |
SMTCoq: A Plug-In for Integrating SMT Solvers into Coq
|
|---|---|
| Autor/in / Beteiligte Person: | Barrett, Clark ; Keller, Chantal ; Reynolds, Andrew ; Ekici, Burak ; Tinelli, Cesare ; Mebsout, Alain ; Katz, Guy ; University of Iowa [Iowa City] ; Paris-Saclay, Université ; Laboratoire de Recherche en Informatique (LRI) ; CentraleSupélec-Université Paris-Sud - Paris 11 (UP11)-Centre National de la Recherche Scientifique (CNRS) ; Vérification d'Algorithmes, Langages et Systèmes (LRI) (VALS - LRI) ; CentraleSupélec-Université Paris-Sud - Paris 11 (UP11)-Centre National de la Recherche Scientifique (CNRS)-CentraleSupélec-Université Paris-Sud - Paris 11 (UP11)-Centre National de la Recherche Scientifique (CNRS) ; Université Paris-Sud - Paris 11 (UP11) ; University, Stanford ; Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS) ; Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-Université Paris-Sud - Paris 11 (UP11)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS) |
| Link: | |
| Quelle: | Computer Aided Verification ISBN: 9783319633893 CAV (2) Computer Aided Verification-29th International Conference Computer Aided Verification-29th International Conference, Jul 2017, Heidelberg, Germany; (2017) |
| Veröffentlichung: | Springer International Publishing, 2017 |
| Medientyp: | unknown |
| ISBN: | 978-3-319-63389-3 (print) |
| DOI: | 10.1007/978-3-319-63390-9_7 |
| Schlagwort: |
|
| Sonstiges: |
|