References

[AFGregoire+11]

Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, and Benjamin Werner. A modular integration of SAT\slash SMT solvers to Coq through proof witnesses. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs (CPP), volume 7086 of Lecture Notes in Computer Science, 135–150. Springer, 2011. doi:10.1007/978-3-642-25379-9_12.

[BBRT17]

Kshitij Bansal, Clark W. Barrett, Andrew Reynolds, and Cesare Tinelli. A new decision procedure for finite sets and cardinality constraints in SMT. CoRR, 2017. arXiv:1702.06259.

[BBFF20]

Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, and Pascal Fontaine. Scalable fine-grained proofs for formula processing. Journal of Automated Reasoning, 64(3):485–510, 2020. URL: https://doi.org/10.1007/s10817-018-09502-y, doi:10.1007/s10817-018-09502-y.

[BFT17]

Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The SMT-LIB Standard: Version 2.6. Technical Report, Department of Computer Science, The University of Iowa, 2017. Available at \tt www.SMT-LIB.org.

[BST07]

Clark W. Barrett, Igor Shikanian, and Cesare Tinelli. An abstract decision procedure for a theory of inductive data types. J. Satisf. Boolean Model. Comput., 3(1-2):21–46, 2007. doi:10.3233/sat190028.

[BdODeharbeF09]

Thomas Bouton, Diego Caminha B. de Oliveira, David Déharbe, and Pascal Fontaine. veriT: An Open, Trustable and Efficient SMT-Solver. In Renate A. Schmidt, editor, Conference on Automated Deduction (CADE), volume 5663 of Lecture Notes in Computer Science, 151–156. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-02959-2_12, doi:10.1007/978-3-642-02959-2_12.

[CGI+18]

Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, and Roberto Sebastiani. Incremental linearization for satisfiability and verification modulo nonlinear arithmetic and transcendental functions. ACM Trans. Comput. Log., 19(3):19:1–19:52, 2018. doi:10.1145/3230639.

[EMT+17]

Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, and Clark W. Barrett. Smtcoq: A plug-in for integrating SMT solvers into coq. In Rupak Majumdar and Viktor Kuncak, editors, Computer Aided Verification (CAV), volume 10427 of Lecture Notes in Computer Science, 126–133. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63390-9_7, doi:10.1007/978-3-319-63390-9_7.

[IEE19]

IEEE. IEEE Standard for Floating-Point Arithmetic. IEEE Std 754-2019 (Revision of IEEE 754-2008), pages 1–84, 2019. doi:10.1109/IEEESTD.2019.8766229.

[MRTB17]

Baoluo Meng, Andrew Reynolds, Cesare Tinelli, and Clark W. Barrett. Relational constraint solving in SMT. In Leonardo de Moura, editor, Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, volume 10395 of Lecture Notes in Computer Science, 148–165. Springer, 2017. doi:10.1007/978-3-319-63046-5_10.

[OKTB23]

Alex Ozdemir, Gereon Kremer, Cesare Tinelli, and Clark Barrett. Satisfiability modulo finite fields. In Constantin Enea and Akash Lal, editors, Computer Aided Verification (CAV), volume 13965 of Lecture Notes in Computer Science, 163–186. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-37703-7_8, doi:10.1007/978-3-031-37703-7_8.

[OPB+24]

Alex Ozdemir, Shankara Pailoor, Alp Bassa, Kostas Ferles, Clark Barrett, and Işıl Dillig. Split gröbner bases for satisfiability modulo finite fields. In Computer Aided Verification (CAV), Lecture Notes in Computer Science. 2024. URL: https://ia.cr/2024/572.

[RB15]

Andrew Reynolds and Jasmin Christian Blanchette. A decision procedure for (co)datatypes in SMT solvers. In Amy P. Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, volume 9195 of Lecture Notes in Computer Science, 197–213. Springer, 2015. doi:10.1007/978-3-319-21401-6_13.

[RISK16]

Andrew Reynolds, Radu Iosif, Cristina Serban, and Tim King. A decision procedure for separation logic in SMT. In Cyrille Artho, Axel Legay, and Doron Peled, editors, Automated Technology for Verification and Analysis - 14th International Symposium, ATVA 2016, Chiba, Japan, October 17-20, 2016, Proceedings, volume 9938 of Lecture Notes in Computer Science, 244–261. 2016. doi:10.1007/978-3-319-46520-3_16.

[SFD21]

Hans-Jörg Schurr, Mathias Fleury, and Martin Desharnais. Reliable reconstruction of fine-grained proofs in a proof assistant. In André Platzer and Geoff Sutcliffe, editors, Conference on Automated Deduction (CADE), volume 12699 of Lecture Notes in Computer Science, 450–467. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-79876-5_26, doi:10.1007/978-3-030-79876-5_26.

[SOR+13]

Aaron Stump, Duckki Oe, Andrew Reynolds, Liana Hadarean, and Cesare Tinelli. SMT proof checking using a logical framework. Formal Methods Syst. Des., 42(1):91–118, 2013. URL: https://doi.org/10.1007/s10703-012-0163-3, doi:10.1007/s10703-012-0163-3.