diff options
Diffstat (limited to 'lsr_refs.bib')
| -rw-r--r-- | lsr_refs.bib | 28 |
1 files changed, 28 insertions, 0 deletions
diff --git a/lsr_refs.bib b/lsr_refs.bib index 4ac943b..1833535 100644 --- a/lsr_refs.bib +++ b/lsr_refs.bib @@ -30,6 +30,21 @@ type = {Standard} } +@InProceedings{armand11_modul_integ_sat_smt_solver, + keywords = {SAT, verification, coq}, + author = {Armand, Michael and Faure, Germain and Grégoire, Benjamin and Keller, Chantal and Théry, Laurent and Werner, Benjamin}, + editor = "Jouannaud, Jean-Pierre +and Shao, Zhong", + title = "A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses", + booktitle = "Certified Programs and Proofs", + year = "2011", + publisher = "Springer Berlin Heidelberg", + address = "Berlin, Heidelberg", + pages = "135--150", + abstract = "We present a way to enjoy the power of SAT and SMT provers in Coq without compromising soundness. This requires these provers to return not only a yes/no answer, but also a proof witness that can be independently rechecked. We present such a checker, written and fully certified in Coq. It is conceived in a modular way, in order to tame the proofs' complexity and to be extendable. It can currently check witnesses from the SAT solver ZChaff and from the SMT solver veriT. Experiments highlight the efficiency of this checker. On top of it, new reflexive Coq tactics have been built that can decide a subset of Coq's logic by calling external provers and carefully checking their answers.", + isbn = "978-3-642-25379-9" +} + @article{aubury96_handel_c_languag_refer_guide, author = {Aubury, Matthew and Page, Ian and Randall, Geoff and Saul, Jonathan and Watts, Robin}, title = {Handel-C Language Reference Guide}, @@ -150,6 +165,19 @@ series = {PLDI 2020} } +@InProceedings{bouton09, + author = {Bouton, Thomas and Caminha B. de Oliveira, Diego and Déharbe, David and Fontaine, Pascal}, + editor = "Schmidt, Renate A.", + title = "veriT: An Open, Trustable and Efficient SMT-Solver", + booktitle = "Automated Deduction -- CADE-22", + year = "2009", + publisher = "Springer Berlin Heidelberg", + address = "Berlin, Heidelberg", + pages = "151--156", + abstract = "This article describes the first public version of the satisfiability modulo theory (SMT) solver veriT. It is open-source, proof-producing, and complete for quantifier-free formulas with uninterpreted functions and difference logic on real numbers and integers.", + isbn = "978-3-642-02959-2" +} + @article{bowen98_handel_c_languag_refer_manual, author = {Bowen, Matthew}, title = {Handel-C Language Reference Manual}, |