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

by Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark Barrett
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.
Reference:
SMTCoq: A Plug-In for Integrating SMT Solvers into Coq (Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, Clark Barrett), In Proceedings of the 29th International Conference on Computer Aided Verification (CAV ’17) (Rupak Majumdar, Viktor Kuncak, eds.), Springer, volume 10426, 2017. (Heidelberg, Germany)
Bibtex Entry:
@inproceedings{EMT+17,
  url       = "http://www.cs.stanford.edu/~barrett/pubs/EMT+17.pdf",
  author    = "Burak Ekici and Alain Mebsout and Cesare Tinelli and Chantal Keller and Guy Katz and Andrew Reynolds and Clark Barrett",
  title     = "{SMTC}oq: A Plug-In for Integrating {SMT} Solvers into {C}oq",
  booktitle = "Proceedings of the 29th International Conference on Computer Aided Verification (CAV '17)",
  volume    = 10426,
  number    = 1,
  editor    = "Rupak Majumdar and Viktor Kuncak",
  pages     = "126--136",
  series    = "Lecture Notes in Computer Science",
  publisher = "Springer",
  month     = jul,
  year      = 2017,
  note      = "Heidelberg, Germany",
  category  = "Conference Publications",
  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.
"
}

Fork me on GitHub