{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T10:22:18Z","timestamp":1768213338387,"version":"3.49.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032156990","type":"print"},{"value":"9783032157003","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:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-15700-3_1","type":"book-chapter","created":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T07:21:57Z","timestamp":1768202517000},"page":"1-20","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Producing Shorter Congruence Closure Proofs in\u00a0a\u00a0State-of-the-Art SMT Solver"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0345-6495","authenticated-orcid":false,"given":"Bruno","family":"Andreotti","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0188-2300","authenticated-orcid":false,"given":"Haniel","family":"Barbosa","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2026,1,13]]},"reference":[{"key":"1_CR1","doi-asserted-by":"publisher","unstructured":"Andreotti, B., Barbosa, H.: Artifact for \u201cproducing shorter congruence closure proofs in a state-of-the-art smt solver\u201d (2025). https:\/\/doi.org\/10.5281\/zenodo.17181344","DOI":"10.5281\/zenodo.17181344"},{"key":"1_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: Tools and Algorithms for the Construction and Analysis of Systems: 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, 22\u201327 April 2023, Proceedings, Part I, pp. 367\u2013386. Springer-Verlag, Berlin, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_19","DOI":"10.1007\/978-3-031-30823-9_19"},{"key":"1_CR3","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: Generating and exploiting automated reasoning proof certificates. Commun. ACM 66(10), 86\u201395 (2023). https:\/\/doi.org\/10.1145\/3587692","DOI":"10.1145\/3587692"},{"key":"1_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24"},{"key":"1_CR5","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: Flexible proof production in an industrial-strength smt solver. In: Automated Reasoning: 11th International Joint Conference, IJCAR 2022, Haifa, Israel, 8\u201310 August 2022, Proceedings, pp. 15\u201335. Springer, Heidelberg (2022). https:\/\/doi.org\/10.1007\/978-3-031-10769-6_3","DOI":"10.1007\/978-3-031-10769-6_3"},{"key":"1_CR6","doi-asserted-by":"publisher","unstructured":"Barbosa, H., Reynolds, A., Ouraoui, D.E., Tinelli, C., Barrett, C.W.: Extending SMT solvers to higher-order logic. In: Fontaine, P. (ed.) Proceedings of Conference on Automated Deduction (CADE). Lecture Notes in Computer Science, vol. 11716, pp. 35\u201354. Springer, Heidelberg (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_3","DOI":"10.1007\/978-3-030-29436-6_3"},{"key":"1_CR7","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). https:\/\/smt-lib.org\/"},{"key":"1_CR8","doi-asserted-by":"publisher","unstructured":"Coutelier, R., Fleury, M., Kov\u00e1cs, L.: Lazy reimplication in chronological backtracking. In: Chakraborty, S., Jiang, J.R. (eds.) 27th International Conference on Theory and Applications of Satisfiability Testing, SAT 2024, Pune, India, 21\u201324 August 2024. LIPIcs, vol.\u00a0305, pp. 9:1\u20139:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2024). https:\/\/doi.org\/10.4230\/LIPICS.SAT.2024.9","DOI":"10.4230\/LIPICS.SAT.2024.9"},{"key":"1_CR9","doi-asserted-by":"publisher","unstructured":"Downey, P.J., Sethi, R., Tarjan, R.E.: Variations on the common subexpression problem. J. ACM 27(4), 758\u2013771 (1980). https:\/\/doi.org\/10.1145\/322217.322228","DOI":"10.1145\/322217.322228"},{"key":"1_CR10","doi-asserted-by":"publisher","unstructured":"Fellner, A., Fontaine, P., Paleo, B.W.: Np-completeness of small conflict set generation for congruence closure. Form. Methods Syst. Des. 51(3), 533\u2013544 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0283-x","DOI":"10.1007\/s10703-017-0283-x"},{"key":"1_CR11","doi-asserted-by":"publisher","unstructured":"Flatt, O., Coward, S., Willsey, M., Tatlock, Z., Panchekha, P.: Small proofs from congruence closure. In: 2022 Formal Methods in Computer-Aided Design (FMCAD), pp. 75\u201383 (2022). https:\/\/doi.org\/10.34727\/2022\/isbn.978-3-85448-053-2_13","DOI":"10.34727\/2022\/isbn.978-3-85448-053-2_13"},{"key":"1_CR12","doi-asserted-by":"publisher","unstructured":"Fontaine, P., Merz, S., Woltzenlogel\u00a0Paleo, B.: Compression of propositional resolution proofs via partial regularization. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) Automated Deduction \u2013 CADE-23, pp. 237\u2013251. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_19","DOI":"10.1007\/978-3-642-22438-6_19"},{"key":"1_CR13","doi-asserted-by":"publisher","unstructured":"Heule, M.J.H., Kiesl, B., Biere, A.: Short proofs without new variables. In: de\u00a0Moura, L. (ed.) Automated Deduction \u2013 CADE 26, pp. 130\u2013147. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_9","DOI":"10.1007\/978-3-319-63046-5_9"},{"key":"1_CR14","unstructured":"Hoenicke, J., Schindler, T.: A simple proof format for SMT. In: D\u00e9harbe, D., Hyv\u00e4rinen, A.E.J. (eds.) International Workshop on Satisfiability Modulo Theories (SMT). CEUR Workshop Proceedings, vol.\u00a03185, pp. 54\u201370. CEUR-WS.org (2022). http:\/\/ceur-ws.org\/Vol-3185\/paper9527.pdf"},{"key":"1_CR15","doi-asserted-by":"publisher","unstructured":"Marques\u00a0Silva, J., Sakallah, K.: Grasp-a new search algorithm for satisfiability. In: Proceedings of International Conference on Computer Aided Design, pp. 220\u2013227 (1996). https:\/\/doi.org\/10.1109\/ICCAD.1996.569607","DOI":"10.1109\/ICCAD.1996.569607"},{"key":"1_CR16","doi-asserted-by":"publisher","unstructured":"Nadel, A.: Introducing intel(r) SAT solver. In: Meel, K.S., Strichman, O. (eds.) 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, Haifa, Israel, 2\u20135 August 2022. LIPIcs, vol.\u00a0236, pp. 8:1\u20138:23. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2022). https:\/\/doi.org\/10.4230\/LIPICS.SAT.2022.8","DOI":"10.4230\/LIPICS.SAT.2022.8"},{"key":"1_CR17","doi-asserted-by":"publisher","unstructured":"Nelson, G., Oppen, D.C.: Fast decision procedures based on congruence closure. J. ACM 27(2), 356\u2013364 (1980). https:\/\/doi.org\/10.1145\/322186.322198","DOI":"10.1145\/322186.322198"},{"key":"1_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/978-3-540-39813-4_5","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R Nieuwenhuis","year":"2003","unstructured":"Nieuwenhuis, R., Oliveras, A.: Congruence closure with integer offsets. In: Vardi, M.Y., Voronkov, A. (eds.) LPAR 2003. LNCS (LNAI), vol. 2850, pp. 78\u201390. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-39813-4_5"},{"key":"1_CR19","doi-asserted-by":"publisher","unstructured":"Nieuwenhuis, R., Oliveras, A.: Proof-producing congruence closure. In: Giesl, J. (ed.) Term Rewriting and Applications. pp. 453\u2013468. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-32033-3_33","DOI":"10.1007\/978-3-540-32033-3_33"},{"key":"1_CR20","doi-asserted-by":"publisher","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving sat and sat modulo theories: from an abstract davis\u2013putnam\u2013logemann\u2013loveland procedure to dpll(t). J. ACM 53(6), 937\u2013977 (2006). https:\/\/doi.org\/10.1145\/1217856.1217859","DOI":"10.1145\/1217856.1217859"},{"key":"1_CR21","doi-asserted-by":"publisher","unstructured":"Otoni, R., Blicha, M., Eugster, P., Hyv\u00e4rinen, A.E.J., Sharygina, N.: Theory-specific proof steps witnessing correctness of SMT executions. In: Design Automation Conference (DAC), pp. 541\u2013546. IEEE (2021). https:\/\/doi.org\/10.1109\/DAC18074.2021.9586272","DOI":"10.1109\/DAC18074.2021.9586272"},{"key":"1_CR22","doi-asserted-by":"publisher","unstructured":"Reeves, J.E., Kiesl-Reiter, B., Heule, M.J.H.: Propositional proof skeletons. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 329\u2013347. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-30823-9_17","DOI":"10.1007\/978-3-031-30823-9_17"},{"key":"1_CR23","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.) Proceedings of Conference on Automated Deduction (CADE). Lecture Notes in Computer Science, vol. 12699, pp. 450\u2013467. Springer, Heidelberg (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_26","DOI":"10.1007\/978-3-030-79876-5_26"},{"key":"1_CR24","doi-asserted-by":"publisher","unstructured":"Tarjan, R.E.: Efficiency of a good but not linear set union algorithm. J. ACM 22(2), 215\u2013225 (1975). https:\/\/doi.org\/10.1145\/321879.321884","DOI":"10.1145\/321879.321884"},{"key":"1_CR25","doi-asserted-by":"publisher","unstructured":"Tate, R., Stepp, M., Tatlock, Z., Lerner, S.: Equality saturation: a new approach to optimization. SIGPLAN Not. 44(1), 264\u2013276 (2009). https:\/\/doi.org\/10.1145\/1594834.1480915","DOI":"10.1145\/1594834.1480915"},{"key":"1_CR26","doi-asserted-by":"publisher","unstructured":"Willsey, M., Nandi, C., Wang, Y.R., Flatt, O., Tatlock, Z., Panchekha, P.: EGG: fast and extensible equality saturation. Proc. ACM Program. Lang. 5(POPL) (2021). https:\/\/doi.org\/10.1145\/3434304","DOI":"10.1145\/3434304"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-15700-3_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,1,12]],"date-time":"2026-01-12T07:21:58Z","timestamp":1768202518000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-15700-3_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032156990","9783032157003"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-15700-3_1","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":"13 January 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rennes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","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":"12 January 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 January 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/VMCAI-2026","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}