mirror of
https://github.com/AdaCore/cvc5.git
synced 2026-02-12 12:32:16 -08:00
283 lines
9.6 KiB
BibTeX
283 lines
9.6 KiB
BibTeX
@string{cade = "Conference on Automated Deduction (CADE)"}
|
||
@string{cpp = "Certified Programs and Proofs (CPP)"}
|
||
@string{cav = "Computer Aided Verification (CAV)"}
|
||
@string{jar = "Journal of Automated Reasoning"}
|
||
@string{lncs = "Lecture Notes in Computer Science"}
|
||
|
||
@article{DBLP:journals/tocl/CimattiGIRS18,
|
||
author = {Alessandro Cimatti and
|
||
Alberto Griggio and
|
||
Ahmed Irfan and
|
||
Marco Roveri and
|
||
Roberto Sebastiani},
|
||
title = {Incremental Linearization for Satisfiability and Verification Modulo
|
||
Nonlinear Arithmetic and Transcendental Functions},
|
||
journal = {{ACM} Trans. Comput. Log.},
|
||
volume = {19},
|
||
number = {3},
|
||
pages = {19:1--19:52},
|
||
year = {2018},
|
||
doi = {10.1145/3230639},
|
||
timestamp = {Fri, 09 Apr 2021 18:33:35 +0200},
|
||
biburl = {https://dblp.org/rec/journals/tocl/CimattiGIRS18.bib},
|
||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||
}
|
||
|
||
|
||
@article{IEEE754,
|
||
author={IEEE},
|
||
journal={IEEE Std 754-2019 (Revision of IEEE 754-2008)},
|
||
title={{IEEE Standard for Floating-Point Arithmetic}},
|
||
year={2019},
|
||
pages={1-84},
|
||
doi={10.1109/IEEESTD.2019.8766229}
|
||
}
|
||
|
||
@article{BansalBRT17,
|
||
author = {Kshitij Bansal and
|
||
Clark W. Barrett and
|
||
Andrew Reynolds and
|
||
Cesare Tinelli},
|
||
title = {A New Decision Procedure for Finite Sets and Cardinality Constraints
|
||
in {SMT}},
|
||
journal = {CoRR},
|
||
volume = {abs/1702.06259},
|
||
year = {2017},
|
||
archivePrefix = {arXiv},
|
||
eprint = {1702.06259},
|
||
timestamp = {Mon, 13 Aug 2018 16:47:11 +0200},
|
||
biburl = {https://dblp.org/rec/journals/corr/BansalBRT17.bib},
|
||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||
}
|
||
|
||
@inproceedings{MengRTB17,
|
||
author = {Baoluo Meng and
|
||
Andrew Reynolds and
|
||
Cesare Tinelli and
|
||
Clark W. Barrett},
|
||
editor = {Leonardo de Moura},
|
||
title = {Relational Constraint Solving in {SMT}},
|
||
booktitle = {Automated Deduction - {CADE} 26 - 26th International Conference on
|
||
Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings},
|
||
series = {Lecture Notes in Computer Science},
|
||
volume = {10395},
|
||
pages = {148--165},
|
||
publisher = {Springer},
|
||
year = {2017},
|
||
doi = {10.1007/978-3-319-63046-5_10},
|
||
timestamp = {Wed, 25 Sep 2019 18:19:14 +0200},
|
||
biburl = {https://dblp.org/rec/conf/cade/MengRTB17.bib},
|
||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||
}
|
||
|
||
@inproceedings{ReynoldsISK16,
|
||
author = {Andrew Reynolds and
|
||
Radu Iosif and
|
||
Cristina Serban and
|
||
Tim King},
|
||
editor = {Cyrille Artho and
|
||
Axel Legay and
|
||
Doron Peled},
|
||
title = {A Decision Procedure for Separation Logic in {SMT}},
|
||
booktitle = {Automated Technology for Verification and Analysis - 14th International
|
||
Symposium, {ATVA} 2016, Chiba, Japan, October 17-20, 2016, Proceedings},
|
||
series = {Lecture Notes in Computer Science},
|
||
volume = {9938},
|
||
pages = {244--261},
|
||
year = {2016},
|
||
doi = {10.1007/978-3-319-46520-3_16},
|
||
timestamp = {Tue, 14 May 2019 10:00:49 +0200},
|
||
biburl = {https://dblp.org/rec/conf/atva/ReynoldsIS016.bib},
|
||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||
}
|
||
|
||
@inproceedings{ReynoldsB15,
|
||
author = {Andrew Reynolds and
|
||
Jasmin Christian Blanchette},
|
||
editor = {Amy P. Felty and
|
||
Aart Middeldorp},
|
||
title = {A Decision Procedure for (Co)datatypes in {SMT} Solvers},
|
||
booktitle = {Automated Deduction - {CADE-25} - 25th International Conference on
|
||
Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings},
|
||
series = {Lecture Notes in Computer Science},
|
||
volume = {9195},
|
||
pages = {197--213},
|
||
publisher = {Springer},
|
||
year = {2015},
|
||
doi = {10.1007/978-3-319-21401-6_13},
|
||
timestamp = {Tue, 14 May 2019 10:00:39 +0200},
|
||
biburl = {https://dblp.org/rec/conf/cade/ReynoldsB15.bib},
|
||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||
}
|
||
|
||
@article{BarrettST07,
|
||
author = {Clark W. Barrett and
|
||
Igor Shikanian and
|
||
Cesare Tinelli},
|
||
title = {An Abstract Decision Procedure for a Theory of Inductive Data Types},
|
||
journal = {J. Satisf. Boolean Model. Comput.},
|
||
volume = {3},
|
||
number = {1-2},
|
||
pages = {21--46},
|
||
year = {2007},
|
||
doi = {10.3233/sat190028},
|
||
timestamp = {Mon, 17 Aug 2020 18:32:39 +0200},
|
||
biburl = {https://dblp.org/rec/journals/jsat/BarrettST07.bib},
|
||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||
}
|
||
|
||
@article{DBLP:journals/fmsd/StumpORHT13,
|
||
author = {Aaron Stump and
|
||
Duckki Oe and
|
||
Andrew Reynolds and
|
||
Liana Hadarean and
|
||
Cesare Tinelli},
|
||
title = {{SMT} proof checking using a logical framework},
|
||
journal = {Formal Methods Syst. Des.},
|
||
volume = {42},
|
||
number = {1},
|
||
pages = {91--118},
|
||
year = {2013},
|
||
url = {https://doi.org/10.1007/s10703-012-0163-3},
|
||
doi = {10.1007/s10703-012-0163-3},
|
||
timestamp = {Tue, 27 Jul 2021 08:54:10 +0200},
|
||
biburl = {https://dblp.org/rec/journals/fmsd/StumpORHT13.bib},
|
||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||
}
|
||
|
||
@TECHREPORT{BarFT-RR-17,
|
||
author = {Clark Barrett and Pascal Fontaine and Cesare Tinelli},
|
||
title = {{The SMT-LIB Standard: Version 2.6}},
|
||
institution = {Department of Computer Science, The University of Iowa},
|
||
year = 2017,
|
||
note = {Available at {\tt www.SMT-LIB.org}}
|
||
}
|
||
|
||
@inproceedings{Bouton2009,
|
||
author = {Thomas Bouton and
|
||
Diego Caminha B. de Oliveira and
|
||
David D{\'{e}}harbe and
|
||
Pascal Fontaine},
|
||
title = {{veriT}: {A}n {O}pen, {T}rustable and {E}fficient {SMT-S}olver},
|
||
booktitle = cade,
|
||
pages = {151--156},
|
||
year = {2009},
|
||
url = {http://dx.doi.org/10.1007/978-3-642-02959-2_12},
|
||
doi = {10.1007/978-3-642-02959-2_12},
|
||
editor = {Renate A. Schmidt},
|
||
series = lncs,
|
||
volume = {5663},
|
||
publisher = {Springer},
|
||
}
|
||
|
||
@inproceedings{Armand2011,
|
||
author = {Micha{\"e}l Armand and
|
||
Germain Faure and
|
||
Benjamin Gr{\'e}goire and
|
||
Chantal Keller and
|
||
Laurent Th{\'e}ry and
|
||
Benjamin Werner},
|
||
title = {A~Modular Integration of {SAT}\slash{SMT} Solvers to {Coq} through
|
||
Proof Witnesses},
|
||
booktitle = cpp,
|
||
pages = {135--150},
|
||
editor = {Jean-Pierre Jouannaud and
|
||
Zhong Shao},
|
||
publisher = {Springer},
|
||
series = lncs,
|
||
volume = {7086},
|
||
year = {2011},
|
||
doi = {10.1007/978-3-642-25379-9_12}
|
||
}
|
||
|
||
@inproceedings{Ekici2017,
|
||
author = {Burak Ekici and
|
||
Alain Mebsout and
|
||
Cesare Tinelli and
|
||
Chantal Keller and
|
||
Guy Katz and
|
||
Andrew Reynolds and
|
||
Clark W. Barrett},
|
||
title = {SMTCoq: {A} Plug-In for Integrating {SMT} Solvers into Coq},
|
||
booktitle = cav,
|
||
pages = {126--133},
|
||
year = {2017},
|
||
url = {https://doi.org/10.1007/978-3-319-63390-9_7},
|
||
doi = {10.1007/978-3-319-63390-9_7},
|
||
editor = {Rupak Majumdar and
|
||
Viktor Kuncak},
|
||
series = lncs,
|
||
volume = {10427},
|
||
publisher = {Springer},
|
||
}
|
||
|
||
@article{Barbosa2020,
|
||
author = {Haniel Barbosa and
|
||
Jasmin Christian Blanchette and
|
||
Mathias Fleury and
|
||
Pascal Fontaine},
|
||
title = {Scalable Fine-Grained Proofs for Formula Processing},
|
||
journal = jar,
|
||
volume = {64},
|
||
number = {3},
|
||
pages = {485--510},
|
||
year = {2020},
|
||
url = {https://doi.org/10.1007/s10817-018-09502-y},
|
||
doi = {10.1007/s10817-018-09502-y},
|
||
timestamp = {Thu, 19 Mar 2020 10:23:41 +0100},
|
||
biburl = {https://dblp.org/rec/journals/jar/BarbosaBFF20.bib},
|
||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||
}
|
||
|
||
@inproceedings{Schurr2021,
|
||
author = {Hans{-}J{\"{o}}rg Schurr and
|
||
Mathias Fleury and
|
||
Martin Desharnais},
|
||
editor = {Andr{\'{e}} Platzer and
|
||
Geoff Sutcliffe},
|
||
title = {Reliable Reconstruction of Fine-grained Proofs in a Proof Assistant},
|
||
booktitle = cade,
|
||
series = lncs,
|
||
volume = {12699},
|
||
pages = {450--467},
|
||
publisher = {Springer},
|
||
year = {2021},
|
||
url = {https://doi.org/10.1007/978-3-030-79876-5_26},
|
||
doi = {10.1007/978-3-030-79876-5_26},
|
||
timestamp = {Mon, 12 Jul 2021 14:18:46 +0200},
|
||
biburl = {https://dblp.org/rec/conf/cade/SchurrFD21.bib},
|
||
bibsource = {dblp computer science bibliography, https://dblp.org}
|
||
}
|
||
|
||
@inproceedings{Ozdemir23,
|
||
author = {Alex Ozdemir and
|
||
Gereon Kremer and
|
||
Cesare Tinelli and
|
||
Clark Barrett},
|
||
editor = {Constantin Enea and
|
||
Akash Lal},
|
||
title = {Satisfiability Modulo Finite Fields},
|
||
booktitle = cav,
|
||
series = lncs,
|
||
volume = {13965},
|
||
pages = {163--186},
|
||
publisher = {Springer},
|
||
year = {2023},
|
||
url = {https://doi.org/10.1007/978-3-031-37703-7_8},
|
||
doi = {10.1007/978-3-031-37703-7_8}
|
||
}
|
||
|
||
@inproceedings{Ozdemir24,
|
||
author = {Alex Ozdemir and
|
||
Shankara Pailoor and
|
||
Alp Bassa and
|
||
Kostas Ferles and
|
||
Clark Barrett and
|
||
Işıl Dillig},
|
||
title = {Split Gröbner Bases for Satisfiability Modulo Finite Fields},
|
||
booktitle = cav,
|
||
series = lncs,
|
||
year = {2024},
|
||
url = {https://ia.cr/2024/572}
|
||
}
|