{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T22:05:16Z","timestamp":1784844316153,"version":"3.55.0"},"publisher-location":"Cham","reference-count":50,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325259","type":"print"},{"value":"9783032325266","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2026,7,24]],"date-time":"2026-07-24T00:00:00Z","timestamp":1784851200000},"content-version":"vor","delay-in-days":204,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>We present the Cooperating Proof Calculus (CPC), an evolving set of proof rules encompassing all inferences used in the mainstream theories of the SMT solver cvc5. CPC consists of 585 proof rules, which are formalized in 8025 lines of definitions in the logical framework Eunoia. Eunoia proofs are independently checkable by the proof checker Ethos. This paper gives a detailed summary of CPC, surveying its proof rules over its major components. Having instrumented cvc5 to generate CPC proofs in Eunoia, we show that the solver is capable of generating fine-grained CPC proofs, with no proof holes, for all benchmarks in the SMT library except those in logics with floating-point arithmetic, which are currently not supported. This results in more than 900 million proof steps using 427 unique proof rules. We also discuss ongoing work in the proof assistants Lean and Isabelle to verify the correctness of CPC.<\/jats:p>","DOI":"10.1007\/978-3-032-32526-6_9","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:47:08Z","timestamp":1784796428000},"page":"188-212","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["The Cooperating Proof Calculus: Comprehensive Proofs for\u00a0an\u00a0SMT Solver"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3529-8682","authenticated-orcid":false,"given":"Andrew","family":"Reynolds","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0829-5056","authenticated-orcid":false,"given":"Hans-J\u00f6rg","family":"Schurr","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0188-2300","authenticated-orcid":false,"given":"Haniel","family":"Barbosa","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-3127-2837","authenticated-orcid":false,"given":"Ofec","family":"Israel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0000-2840-3109","authenticated-orcid":false,"given":"Jibiana Zoe","family":"Jakpor","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1825-0097","authenticated-orcid":false,"given":"Hanna","family":"Lachnitt","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1414-7073","authenticated-orcid":false,"given":"Abdalrhman","family":"Mohamed","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2600-5283","authenticated-orcid":false,"given":"Aina","family":"Niemetz","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7142-6258","authenticated-orcid":false,"given":"Mathias","family":"Preiner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2972-6695","authenticated-orcid":false,"given":"Yoni","family":"Zohar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-7999-5763","authenticated-orcid":false,"given":"Robert","family":"Jones","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9522-3084","authenticated-orcid":false,"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6726-775X","authenticated-orcid":false,"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"9_CR1","doi-asserted-by":"publisher","unstructured":"Alur, R., et al.: Syntax-guided synthesis. In: Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013, pp.\u00a01\u20138. IEEE (2013). https:\/\/doi.org\/10.1109\/FMCAD.2013.6679385","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"9_CR2","doi-asserted-by":"publisher","unstructured":"Andreotti, B., Lachnitt, H., Barbosa, H.: Carcara: An efficient proof checker and elaborator for SMT proofs in the Alethe format. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for Construction and Analysis of Systems (TACAS), Part I. Lecture Notes in Computer Science, vol. 13993, pp. 367\u2013386. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_19","DOI":"10.1007\/978-3-031-30823-9_19"},{"key":"9_CR3","doi-asserted-by":"publisher","unstructured":"Assaf, A., et al.: Dedukti: a logical framework based on the $$\\lambda $$$$\\Pi $$-calculus modulo theory. CoRR abs\/2311.07185 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2311.07185","DOI":"10.48550\/ARXIV.2311.07185"},{"key":"9_CR4","doi-asserted-by":"publisher","unstructured":"Bansal, K., Reynolds, A., Barrett, C.W., Tinelli, C.: A new decision procedure for finite sets and cardinality constraints in SMT. In: Olivetti, N., Tiwari, A. (eds.) Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings. Lecture Notes in Computer Science, vol.\u00a09706, pp. 82\u201398. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_7","DOI":"10.1007\/978-3-319-40229-1_7"},{"key":"9_CR5","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: Flexible proof production in an industrial-strength SMT solver. In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13385, pp. 15\u201335. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_3","DOI":"10.1007\/978-3-031-10769-6_3"},{"key":"9_CR6","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)"},{"key":"9_CR7","doi-asserted-by":"publisher","unstructured":"Barrett, C.W., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings. Lecture Notes in Computer Science, vol.\u00a06806, pp. 171\u2013177. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14","DOI":"10.1007\/978-3-642-22110-1_14"},{"issue":"1\u20132","key":"9_CR8","doi-asserted-by":"publisher","first-page":"21","DOI":"10.3233\/SAT190028","volume":"3","author":"CW Barrett","year":"2007","unstructured":"Barrett, C.W., Shikanian, I., Tinelli, C.: An abstract decision procedure for a theory of inductive data types. J. Satisf. Boolean Model. Comput. 3(1\u20132), 21\u201346 (2007). https:\/\/doi.org\/10.3233\/SAT190028","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"9_CR9","doi-asserted-by":"publisher","unstructured":"Barrett, C.W., Tinelli, C., Deters, M., Liang, T., Reynolds, A., Tsiskaridze, N.: Efficient solving of string constraints for security analysis. In: Scherlis, W.L., Brumley, D. (eds.) Proceedings of the Symposium and Bootcamp on the Science of Security, Pittsburgh, PA, USA, April 19-21, 2016, pp.\u00a04\u20136. ACM (2016). https:\/\/doi.org\/10.1145\/2898375.2898393","DOI":"10.1145\/2898375.2898393"},{"key":"9_CR10","doi-asserted-by":"publisher","unstructured":"Berger, Z., et al.: Bit-precise reasoning with parametric bit-vectors. In: Berg, J., Nordstr\u00f6m, J. (eds.) 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0341, pp. 4:1\u20134:24. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2025). https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2025.4","DOI":"10.4230\/LIPIcs.SAT.2025.4"},{"key":"9_CR11","doi-asserted-by":"publisher","unstructured":"Biere, A., Faller, T., Fazekas, K., Fleury, M., Froleyks, N., Pollitt, F.: CaDiCaL 2.0. In: Computer Aided Verification (CAV), Part I, pp. 133\u2013152. Springer-Verlag, Berlin, Heidelberg (2024). https:\/\/doi.org\/10.1007\/978-3-031-65627-9_7","DOI":"10.1007\/978-3-031-65627-9_7"},{"key":"9_CR12","doi-asserted-by":"publisher","unstructured":"Blanchette, J.C., Nipkow, T.: Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings. Lecture Notes in Computer Science, vol.\u00a06172, pp. 131\u2013146. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-14052-5_11","DOI":"10.1007\/978-3-642-14052-5_11"},{"key":"9_CR13","doi-asserted-by":"publisher","unstructured":"Bouchet, M., et al.: Block public access: trust safety verification of access control policies. In: Devanbu, P., Cohen, M.B., Zimmermann, T. (eds.) ESEC\/FSE \u201920: 28th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, Virtual Event, USA, November 8-13, 2020, pp. 281\u2013291. ACM (2020). https:\/\/doi.org\/10.1145\/3368089.3409728","DOI":"10.1145\/3368089.3409728"},{"key":"9_CR14","doi-asserted-by":"publisher","unstructured":"Bouton, T., Oliveira, D.C.B.D., D\u00e9harbe, D., Fontaine, P.: verit: An open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings. Lecture Notes in Computer Science, vol.\u00a05663, pp. 151\u2013156. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_12","DOI":"10.1007\/978-3-642-02959-2_12"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Brzozowski, J.A.: Derivatives of regular expressions. J. ACM (1964)","DOI":"10.1145\/321239.321249"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-642-31759-0_19","volume-title":"Model Checking Software","author":"J Christ","year":"2012","unstructured":"Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: an interpolating SMT solver. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol. 7385, pp. 248\u2013254. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31759-0_19"},{"key":"9_CR17","doi-asserted-by":"publisher","unstructured":"Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Invariant checking of NRA transition systems via incremental reduction to LRA with EUF. In: Legay, A., Margaria, T. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10205, pp. 58\u201375 (2017).https:\/\/doi.org\/10.1007\/978-3-662-54577-5_4","DOI":"10.1007\/978-3-662-54577-5_4"},{"issue":"1","key":"9_CR18","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/S00236-025-00515-W","volume":"63","author":"A Coltellacci","year":"2026","unstructured":"Coltellacci, A., Andreotti, B., Barbosa, H., Dowek, G., Merz, S.: Reconstruction of SMT proofs with Lambdapi. Acta Informatica 63(1), 8 (2026). https:\/\/doi.org\/10.1007\/S00236-025-00515-W","journal-title":"Acta Informatica"},{"key":"9_CR19","doi-asserted-by":"publisher","unstructured":"Coltellacci, A., Merz, S.: Checking linear integer arithmetic proofs in Lambdapi. In: Thiemann, R., Weidenbach, C. (eds.) Frontiers of Combining Systems (FroCoS). Lecture Notes in Computer Science, vol. 15979, pp. 367\u2013385. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-032-04167-8_20","DOI":"10.1007\/978-3-032-04167-8_20"},{"key":"9_CR20","doi-asserted-by":"publisher","unstructured":"Cruz-Filipe, L., Heule, M.J.H., Jr., W.A.H., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: de\u00a0Moura, L. (ed.) Proc. Conference on Automated Deduction (CADE). Lecture Notes in Computer Science, vol. 10395, pp. 220\u2013236. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_14","DOI":"10.1007\/978-3-319-63046-5_14"},{"key":"9_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-662-54577-5_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Cruz-Filipe","year":"2017","unstructured":"Cruz-Filipe, L., Marques-Silva, J., Schneider-Kamp, P.: Efficient certified resolution proof checking. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 118\u2013135. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_7"},{"key":"9_CR22","volume-title":"Automated Reasoning - 13th International Joint Conference, IJCAR 2026","author":"C Dunne","year":"2026","unstructured":"Dunne, C., Burel, G.: Automatically translating proof systems for SMT solvers to the lambda pi calculus. In: Biere, A., Lutz, C., Negri, S. (eds.) Automated Reasoning - 13th International Joint Conference, IJCAR 2026. Springer, Lecture Notes in Computer Science (2026)"},{"key":"9_CR23","doi-asserted-by":"publisher","unstructured":"Hitarth, S., Codel, C.R., Lachnitt, H., Dutertre, B.: Extending DRAT to SMT. In: Narodytska, N., R\u00fcmmer, P. (eds.) Formal Methods in Computer-Aided Design, FMCAD 2024, Prague, Czech Republic, October 15-18, 2024, pp. 1\u201311. IEEE (2024). https:\/\/doi.org\/10.34727\/2024\/ISBN.978-3-85448-065-5_8","DOI":"10.34727\/2024\/ISBN.978-3-85448-065-5_8"},{"key":"9_CR24","unstructured":"Hoenicke, J., Schindler, T.: A simple proof format for SMT. In: D\u00e9harbe, D., Hyv\u00e4rinen, A.E.J. (eds.) Proceedings of the 20th Internal Workshop on Satisfiability Modulo Theories co-located with the 11th International Joint Conference on Automated Reasoning (IJCAR 2022) part of the 8th Federated Logic Conference (FLoC 2022), Haifa, Israel, August 11\u201312, 2022. CEUR Workshop Proceedings, vol.\u00a03185, pp. 54\u201370. CEUR-WS.org (2022). https:\/\/ceur-ws.org\/Vol-3185\/paper9527.pdf"},{"key":"9_CR25","volume-title":"Automated Reasoning - 13th International Joint Conference, IJCAR 2026","author":"O Israel","year":"2026","unstructured":"Israel, O., et al.: Checking regular expressions in cvc5 proofs. In: Biere, A., Lutz, C., Negri, S. (eds.) Automated Reasoning - 13th International Joint Conference, IJCAR 2026. Springer, Lecture Notes in Computer Science (2026)"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"516","DOI":"10.1007\/978-3-319-94205-6_34","volume-title":"Automated Reasoning","author":"B Kiesl","year":"2018","unstructured":"Kiesl, B., Rebola-Pardo, A., Heule, M.J.H.: Extended resolution simulates DRAT. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 516\u2013531. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_34"},{"key":"9_CR27","doi-asserted-by":"publisher","unstructured":"Kremer, G., \u00c1brah\u00e1m, E., England, M., Davenport, J.H.: On the implementation of cylindrical algebraic coverings for satisfiability modulo theories solving. In: Schneider, C., Marin, M., Negru, V., Zaharie, D. (eds.) 23rd International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2021, Timisoara, Romania, December 7-10, 2021, pp. 37\u201339. IEEE (2021). https:\/\/doi.org\/10.1109\/SYNASC54541.2021.00018","DOI":"10.1109\/SYNASC54541.2021.00018"},{"key":"9_CR28","doi-asserted-by":"publisher","unstructured":"Kremer, G., Reynolds, A., Barrett, C.W., Tinelli, C.: Cooperating techniques for solving nonlinear real arithmetic in the cvc5 SMT solver (system description). In: Blanchette, J., Kov\u00e1cs, L., Pattinson, D. (eds.) Automated Reasoning - 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Proceedings. Lecture Notes in Computer Science, vol. 13385, pp. 95\u2013105. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_7","DOI":"10.1007\/978-3-031-10769-6_7"},{"key":"9_CR29","doi-asserted-by":"publisher","unstructured":"Lachnitt, H., et al.: Isarare: Automatic verification of SMT rewrites in Isabelle\/HOL. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I. Lecture Notes in Computer Science, vol. 14570, pp. 311\u2013330. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-57246-3_17","DOI":"10.1007\/978-3-031-57246-3_17"},{"key":"9_CR30","doi-asserted-by":"publisher","unstructured":"Lachnitt, H., et al.: Improving the SMT proof reconstruction pipeline in Isabelle\/HOL. In: Forster, Y., Keller, C. (eds.) 16th International Conference on Interactive Theorem Proving, ITP 2025, Reykjavik, Iceland, September 28 - October 1, 2025. LIPIcs, vol.\u00a0352, pp. 26:1\u201326:22. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2025). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2025.26","DOI":"10.4230\/LIPICS.ITP.2025.26"},{"key":"9_CR31","doi-asserted-by":"publisher","unstructured":"Lammich, P.: Efficient verified (UN)SAT certificate checking. In: de\u00a0Moura, L. (ed.) Proc. Conference on Automated Deduction (CADE). Lecture Notes in Computer Science, vol. 10395, pp. 237\u2013254. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_15","DOI":"10.1007\/978-3-319-63046-5_15"},{"key":"9_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"646","DOI":"10.1007\/978-3-319-08867-9_43","volume-title":"Computer Aided Verification","author":"T Liang","year":"2014","unstructured":"Liang, T., Reynolds, A., Tinelli, C., Barrett, C., Deters, M.: A DPLL(T) theory solver for a theory of strings and regular expressions. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 646\u2013662. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_43"},{"key":"9_CR33","doi-asserted-by":"publisher","unstructured":"Mohamed, A., et al.: lean-smt: An SMT tactic for discharging proof goals in Lean. In: Piskac, R., Rakamaric, Z. (eds.) Computer Aided Verification - 37th International Conference, CAV 2025, Zagreb, Croatia, July 23-25, 2025, Proceedings, Part III. Lecture Notes in Computer Science, vol. 15933, pp. 197\u2013212. Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-98682-6_11","DOI":"10.1007\/978-3-031-98682-6_11"},{"key":"9_CR34","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"625","DOI":"10.1007\/978-3-030-79876-5_37","volume-title":"Automated Deduction \u2013 CADE 28","author":"L Moura","year":"2021","unstructured":"Moura, L., Ullrich, S.: The lean 4 theorem prover and programming language. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 625\u2013635. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_37"},{"key":"9_CR35","doi-asserted-by":"publisher","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings, pp. 337\u2013340. Lecture Notes in Computer Science, Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9_CR36","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL - A Proof Assistant for Higher-Order Logic, LNCS, vol.\u00a02283. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"9_CR37","doi-asserted-by":"publisher","unstructured":"N\u00f6tzli, A., et al.: Reconstructing fine-grained proofs of rewrites using a domain-specific language. In: Griggio, A., Rungta, N. (eds.) 22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, October 17-21, 2022, pp. 65\u201374. IEEE (2022). https:\/\/doi.org\/10.34727\/2022\/ISBN.978-3-85448-053-2_12","DOI":"10.34727\/2022\/ISBN.978-3-85448-053-2_12"},{"key":"9_CR38","doi-asserted-by":"publisher","unstructured":"N\u00f6tzli, A., et al.: Syntax-guided rewrite rule enumeration for SMT solvers. In: Janota, M., Lynce, I. (eds.) Theory and Applications of Satisfiability Testing - SAT 2019 - 22nd International Conference, SAT 2019, Lisbon, Portugal, July 9-12, 2019, Proceedings. LNCS, vol. 11628, pp. 279\u2013297. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-24258-9_20","DOI":"10.1007\/978-3-030-24258-9_20"},{"key":"9_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-030-25543-5_5","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2019","unstructured":"Reynolds, A., Barbosa, H., N\u00f6tzli, A., Barrett, C., Tinelli, C.: cvc4sy: Smart and fast term enumeration for syntax-guided synthesis. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 74\u201383. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_5"},{"key":"9_CR40","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-319-21401-6_13","volume-title":"Automated Deduction \u2013 CADE-25","author":"A Reynolds","year":"2015","unstructured":"Reynolds, A., Blanchette, J.C.: A decision procedure for (Co)datatypes in SMT solvers. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 197\u2013213. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_13"},{"key":"9_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-662-46081-8_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A Reynolds","year":"2015","unstructured":"Reynolds, A., Kuncak, V.: Induction for SMT solvers. In: D\u2019Souza, D., Lal, A., Larsen, K.G. (eds.) VMCAI 2015. LNCS, vol. 8931, pp. 80\u201398. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46081-8_5"},{"key":"9_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-030-25543-5_2","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2019","unstructured":"Reynolds, A., N\u00f6tzli, A., Barrett, C., Tinelli, C.: High-level abstractions for simplifying extended string constraints in SMT. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 23\u201342. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_2"},{"key":"9_CR43","unstructured":"Reynolds, A., Schurr, H.J., Soldevila, M., Tinelli, C.: The ethos user manual (2026). https:\/\/github.com\/cvc5\/ethos\/blob\/main\/user_manual.md"},{"key":"9_CR44","volume-title":"Automated Reasoning - 13th International Joint Conference, IJCAR 2026","author":"A Reynolds","year":"2026","unstructured":"Reynolds, A., Schurr, H.J., Soldevila, M., Barbosa, H., Barrett, C., Tinelli, C.: Ethos: a fast proof checker for the Eunoia logical framework. In: Biere, A., Lutz, C., Negri, S. (eds.) Automated Reasoning - 13th International Joint Conference, IJCAR 2026. Springer, Lecture Notes in Computer Science (2026)"},{"key":"9_CR45","doi-asserted-by":"publisher","unstructured":"Reynolds, A., Tinelli, C., Jovanovic, D., Barrett, C.W.: Designing theory solvers with extensions. In: Dixon, C., Finger, M. (eds.) Frontiers of Combining Systems - 11th International Symposium, FroCoS 2017, Bras\u00edlia, Brazil, September 27\u201329, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10483, pp. 22\u201340. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-66167-4_2","DOI":"10.1007\/978-3-319-66167-4_2"},{"key":"9_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-319-63390-9_24","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2017","unstructured":"Reynolds, A., Woo, M., Barrett, C., Brumley, D., Liang, T., Tinelli, C.: Scaling Up DPLL(T) string solvers using context-dependent simplification. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 453\u2013474. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_24"},{"key":"9_CR47","doi-asserted-by":"publisher","unstructured":"Schurr, H., Fleury, M., Barbosa, H., Fontaine, P.: Alethe: Towards a generic SMT proof format (extended abstract). In: Keller, C., Fleury, M. (eds.) Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, PxTP 2021, Pittsburg, PA, USA, July 11, 2021. EPTCS, vol.\u00a0336, pp. 49\u201354 (2021). https:\/\/doi.org\/10.4204\/EPTCS.336.6","DOI":"10.4204\/EPTCS.336.6"},{"key":"9_CR48","doi-asserted-by":"publisher","unstructured":"Schurr, H., Fleury, M., Desharnais, M.: Reliable reconstruction of fine-grained proofs in a proof assistant. In: Platzer, A., Sutcliffe, G. (eds.) Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12699, pp. 450\u2013467. Springer (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_26","DOI":"10.1007\/978-3-030-79876-5_26"},{"issue":"1","key":"9_CR49","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/S10703-012-0163-3","volume":"42","author":"A Stump","year":"2013","unstructured":"Stump, A., Oe, D., Reynolds, A., Hadarean, L., Tinelli, C.: SMT proof checking using a logical framework. Formal Methods Syst. Des. 42(1), 91\u2013118 (2013). https:\/\/doi.org\/10.1007\/S10703-012-0163-3","journal-title":"Formal Methods Syst. Des."},{"key":"9_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-319-09284-3_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"N Wetzler","year":"2014","unstructured":"Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422\u2013429. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-09284-3_31"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32526-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T08:47:13Z","timestamp":1784796433000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32526-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325259","9783032325266"],"references-count":50,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32526-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"24 July 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","label":"Disclosure of Interests","group":{"name":"EthicsHeading","label":"Ethics"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 July 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"38","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/program","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}