{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,24]],"date-time":"2026-02-24T00:10:35Z","timestamp":1771891835058,"version":"3.50.1"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031308222","type":"print"},{"value":"9783031308239","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,4,22]],"date-time":"2023-04-22T00:00:00Z","timestamp":1682121600000},"content-version":"vor","delay-in-days":111,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Proofs from SMT solvers ensure correctness independently from implementation, which is often a requirement when solvers are used in safety-critical applications or proof assistants. Alethe is an established SMT proof format generated by the solvers veriT and cvc5, with reconstruction support in the proof assistants Isabelle\/HOL and Coq. The format is close to SMT-LIB and allows both coarse- and fine-grained steps, facilitating proof production. However, it lacks a stand-alone checker, which harms its usability and hinders its adoption. Moreover, the coarse-grained steps can be too expensive to check and lead to verification failures. We present<jats:sc>Carcara<\/jats:sc>, an independent proof checker and elaborator for Alethe, implemented in Rust. It aims to increase the adoption of the format by providing push-button proof-checking for Alethe proofs, focusing on efficiency and usability; and by providing elaboration for coarse-grained steps into fine-grained ones, increasing the potential success rate of checking Alethe proofs in performance-critical validators, such as proof assistants. We evaluate<jats:sc>Carcara<\/jats:sc>over a large set of Alethe proofs generated from SMT-LIB problems and show that it has good performance and its elaboration techniques can make proofs easier to check.<\/jats:p>","DOI":"10.1007\/978-3-031-30823-9_19","type":"book-chapter","created":{"date-parts":[[2023,4,21]],"date-time":"2023-04-21T20:19:12Z","timestamp":1682108352000},"page":"367-386","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Carcara: An Efficient Proof Checker and Elaborator for SMT Proofs in the Alethe Format"],"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-3355-7828","authenticated-orcid":false,"given":"Hanna","family":"Lachnitt","sequence":"additional","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":[[2023,4,22]]},"reference":[{"key":"19_CR1","unstructured":"GNU Multiple Precision Arithmetic Library. http:\/\/gmplib.org\/, Oct 2022."},{"key":"19_CR2","unstructured":"The Alethe Proof Format: A Speculative Specification and Reference. https:\/\/verit.loria.fr\/documentation\/alethe-spec.pdf, Oct 2022."},{"key":"19_CR3","unstructured":"Bruno Andreotti, Hanna Lachnitt, and Haniel Barbosa. Carcara artifact, 2023. zenodo, https:\/\/doi.org\/10.5281\/zenodo.7574451."},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"Micha\u00ebl Armand, Germain Faure, Benjamin Gr\u00e9goire, Chantal Keller, Laurent Th\u00e9ry, and Benjamin Werner. A modular integration of SAT\/SMT solvers to coq through proof witnesses. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, volume 7086 of Lecture Notes in Computer Science, pages 135\u2013150. Springer, 2011.","DOI":"10.1007\/978-3-642-25379-9_12"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Haniel Barbosa, Clark\u00a0W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres N\u00f6tzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. cvc5: A versatile and industrial-strength SMT solver. In Dana Fisman and Grigore Rosu, editors, Tools and Algorithms for Construction and Analysis of Systems (TACAS), Part I, volume 13243 of Lecture Notes in Computer Science, pages 415\u2013442. Springer, 2022.","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Haniel Barbosa, Jasmin\u00a0Christian Blanchette, Mathias Fleury, and Pascal Fontaine. Scalable fine-grained proofs for formula processing. Journal of Automated Reasoning, 64(3):485\u2013510, 2020.","DOI":"10.1007\/s10817-018-09502-y"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres N\u00f6tzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, and Clark\u00a0W. Barrett. Flexible proof production in an industrial-strength SMT solver. In Jasmin Blanchette, Laura Kov\u00e1cs, and Dirk Pattinson, editors, International Joint Conference on Automated Reasoning (IJCAR), volume 13385 of Lecture Notes in Computer Science, pages 15\u201335. Springer, 2022.","DOI":"10.1007\/978-3-031-10769-6_3"},{"key":"19_CR8","unstructured":"Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org, 2016."},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Clark\u00a0W. Barrett, Roberto Sebastiani, Sanjit\u00a0A. Seshia, and Cesare Tinelli. Satisfiability modulo theories. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability - Second Edition, volume 336 of Frontiers in Artificial Intelligence and Applications, pages 1267\u20131329. IOS Press, 2021.","DOI":"10.3233\/FAIA201017"},{"key":"19_CR10","unstructured":"Fr\u00e9d\u00e9ric Besson, Pascal Fontaine, and Laurent Th\u00e9ry. A flexible proof format for SMT: a proposal. In Workshop on Proof eXchange for Theorem Proving (PxTP), 2011."},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Jasmin\u00a0Christian Blanchette, Sascha B\u00f6hme, and Lawrence\u00a0C. Paulson. Extending sledgehammer with SMT solvers. Journal of Automated Reasoning, 51(1):109\u2013128, 2013.","DOI":"10.1007\/s10817-013-9278-5"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Sascha B\u00f6hme, Anthony C.\u00a0J. Fox, Thomas Sewell, and Tjark Weber. Reconstruction of z3\u2019s bit-vector proofs in HOL4 and isabelle\/hol. In Jean-Pierre Jouannaud and Zhong Shao, editors, Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings, volume 7086 of Lecture Notes in Computer Science, pages 183\u2013198. Springer, 2011.","DOI":"10.1007\/978-3-642-25379-9_15"},{"key":"19_CR13","doi-asserted-by":"crossref","unstructured":"Thomas Bouton, Diego Caminha\u00a0B. de\u00a0Oliveira, David D\u00e9harbe, and Pascal Fontaine. veriT: An Open, Trustable and Efficient SMT-Solver. In Renate\u00a0A. Schmidt, editor, Conference on Automated Deduction (CADE), volume 5663 of Lecture Notes in Computer Science, pages 151\u2013156. Springer, 2009.","DOI":"10.1007\/978-3-642-02959-2_12"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Lilian Burdy and David D\u00e9harbe. Teaching an old dog new tricks - the drudges of the interactive prover in atelier B. In Michael\u00a0J. Butler, Alexander Raschke, Thai\u00a0Son Hoang, and Klaus Reichl, editors, Abstract State Machines, Alloy, B, TLA, VDM, and Z - 6th International Conference, ABZ 2018, Southampton, UK, June 5-8, 2018, Proceedings, volume 10817 of Lecture Notes in Computer Science, pages 415\u2013419. Springer, 2018.","DOI":"10.1007\/978-3-319-91271-4_33"},{"key":"19_CR15","unstructured":"Leonardo\u00a0Mendon\u00e7a de\u00a0Moura and Nikolaj Bj\u00f8rner. Proofs and refutations, and Z3. In Piotr Rudnicki, Geoff Sutcliffe, Boris Konev, Renate\u00a0A. Schmidt, and Stephan Schulz, editors, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) Workshops, volume 418 of CEUR Workshop Proceedings. CEUR-WS.org, 2008."},{"key":"19_CR16","doi-asserted-by":"crossref","unstructured":"Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, and Clark\u00a0W. Barrett. Smtcoq: A plug-in for integrating SMT solvers into coq. In Rupak Majumdar and Viktor Kuncak, editors, Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, volume 10427 of Lecture Notes in Computer Science, pages 126\u2013133. Springer, 2017.","DOI":"10.1007\/978-3-319-63390-9_7"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"Herbert\u00a0B. Enderton. A mathematical introduction to logic. Academic Press, 2 edition, 2001.","DOI":"10.1016\/B978-0-08-049646-7.50005-9"},{"key":"19_CR18","unstructured":"G.\u00a0Farkas. A Fourier-f\u00e9le mechanikai elv alkamaz\u00e1sai. Mathematikai\u00e9s Term\u00e9szettudom\u00e1nyi \u00c9rtes\u00edt\u00f6, 12:457\u2013472, 1894. reference from Schrijver\u2019s Combinatorial Optimization textbook (Hungarian)."},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Mathias Fleury. Optimizing a verified SAT solver. In Julia\u00a0M. Badger and Kristin\u00a0Yvonne Rozier, editors, NASA Formal Methods - 11th International Symposium, NFM 2019, Houston, TX, USA, May 7-9, 2019, Proceedings, volume 11460 of Lecture Notes in Computer Science, pages 148\u2013165. Springer, 2019.","DOI":"10.1007\/978-3-030-20652-9_10"},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"Mathias Fleury, Jasmin\u00a0Christian Blanchette, and Peter Lammich. A verified SAT solver with watched literals using imperative HOL. In June Andronick and Amy\u00a0P. Felty, editors, Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018, pages 158\u2013171.ACM, 2018.","DOI":"10.1145\/3176245.3167080"},{"key":"19_CR21","doi-asserted-by":"crossref","unstructured":"Allen\u00a0Van Gelder. Verifying RUP proofs of propositional unsatisfiability. In International Symposium on Artificial Intelligence and Mathematics (ISAIM), 2008.","DOI":"10.1007\/978-3-540-72788-0_31"},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"Robert Harper, Furio Honsell, and Gordon\u00a0D. Plotkin. A framework for defining logics. J. ACM, 40(1):143\u2013184, 1993.","DOI":"10.1145\/138027.138060"},{"key":"19_CR23","unstructured":"Marijn J.\u00a0H. Heule. The DRAT format and drat-trim checker. CoRR, abs\/1610.06229, 2016."},{"key":"19_CR24","unstructured":"Jochen Hoenicke and Tanja Schindler. A simple proof format for SMT. In David D\u00e9harbe and Antti E.\u00a0J. Hyv\u00e4rinen, editors, International Workshop on Satisfiability Modulo Theories (SMT), volume 3185 of CEUR Workshop Proceedings, pages 54\u201370. CEUR-WS.org, 2022."},{"key":"19_CR25","unstructured":"Gabriel Hondet and Fr\u00e9d\u00e9ric Blanqui. The new rewriting engine of dedukti (system description). In Zena\u00a0M. Ariola, editor, International Conference on Formal Structures for Computation and Deduction (FSCD), volume 167 of LIPIcs, pages 35:1\u201335:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 2020."},{"key":"19_CR26","doi-asserted-by":"crossref","unstructured":"Antti E.\u00a0J. Hyv\u00e4rinen, Matteo Marescotti, Leonardo Alt, and Natasha Sharygina. Opensmt2: An SMT solver for multi-core and cloud computing. In Nadia Creignou and Daniel\u00a0Le Berre, editors, Theory and Applications of Satisfiability Testing (SAT), volume 9710 of Lecture Notes in Computer Science, pages 547\u2013553. Springer, 2016.","DOI":"10.1007\/978-3-319-40970-2_35"},{"key":"19_CR27","doi-asserted-by":"crossref","unstructured":"Shuanglong Kan, Anthony\u00a0Widjaja Lin, Philipp R\u00fcmmer, and Micha Schrader. Certistr: a certified string solver. In Andrei Popescu and Steve Zdancewic, editors, Certified Programs and Proofs (CPP), pages 210\u2013224. ACM, 2022.","DOI":"10.1145\/3497775.3503691"},{"key":"19_CR28","doi-asserted-by":"crossref","unstructured":"Guy Katz, Clark\u00a0W. Barrett, Cesare Tinelli, Andrew Reynolds, and Liana Hadarean. Lazy proofs for dpll(t)-based SMT solvers. In Ruzica Piskac and Muralidhar Talupur, editors, Formal Methods In Computer-Aided Design (FMCAD), pages 93\u2013100. IEEE, 2016.","DOI":"10.1109\/FMCAD.2016.7886666"},{"key":"19_CR29","doi-asserted-by":"crossref","unstructured":"Greg Nelson and Derek\u00a0C. Oppen. Fast Decision Procedures Based on Congruence Closure. J. ACM, 27(2):356\u2013364, 1980.","DOI":"10.1145\/322186.322198"},{"key":"19_CR30","doi-asserted-by":"crossref","unstructured":"Aina Niemetz, Mathias Preiner, and Clark\u00a0W. Barrett. Murxla: A modular and highly extensible API fuzzer for SMT solvers. In Sharon Shoham and Yakir Vizel, editors, Computer Aided Verification (CAV), Part II, volume 13372 of Lecture Notes in Computer Science, pages 92\u2013106. Springer, 2022.","DOI":"10.1007\/978-3-031-13188-2_5"},{"key":"19_CR31","doi-asserted-by":"crossref","unstructured":"Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. Solving sat and sat modulo theories: From an abstract davis\u2013putnam\u2013logemann\u2013loveland procedure to dpll(t). J. ACM, 53(6):937\u2013977, November 2006.","DOI":"10.1145\/1217856.1217859"},{"key":"19_CR32","unstructured":"Andres N\u00f6tzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, and Clark Barrett. Reconstructing fine-grained proofs of complex rewrites using a domain-specific language. In Alberto Griggio and Neha Rungta, editors, Formal Methods In Computer-Aided Design (FMCAD), 2022. To appear."},{"key":"19_CR33","doi-asserted-by":"crossref","unstructured":"Duckki Oe, Aaron Stump, Corey Oliver, and Kevin Clancy. versat: A verified modern SAT solver. In Viktor Kuncak and Andrey Rybalchenko, editors, Verification, Model Checking, and Abstract Interpretation (VMCAI), volume 7148 of Lecture Notes in Computer Science, pages 363\u2013378. Springer, 2012.","DOI":"10.1007\/978-3-642-27940-9_24"},{"key":"19_CR34","doi-asserted-by":"crossref","unstructured":"Rodrigo Otoni, Martin Blicha, Patrick Eugster, Antti E.\u00a0J. Hyv\u00e4rinen, and Natasha Sharygina. Theory-specific proof steps witnessing correctness of SMT executions. In 58th ACM\/IEEE Design Automation Conference, DAC 2021, San Francisco, CA, USA, December 5-9, 2021, pages 541\u2013546. IEEE, 2021.","DOI":"10.1109\/DAC18074.2021.9586272"},{"key":"19_CR35","doi-asserted-by":"crossref","unstructured":"Hans-J\u00f6rg Schurr, Mathias Fleury, Haniel Barbosa, and Pascal Fontaine. Alethe: Towards a generic SMT proof format (extended abstract). In Chantal Keller and Mathias Fleury, editors, Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, PxTP 2021, Pittsburg, PA, USA, July 11, 2021, volume 336 of EPTCS, pages 49\u201354, 2021.","DOI":"10.4204\/EPTCS.336.6"},{"key":"19_CR36","doi-asserted-by":"crossref","unstructured":"Hans-J\u00f6rg Schurr, Mathias Fleury, and Martin Desharnais. Reliable reconstruction of fine-grained proofs in a proof assistant. In Andr\u00e9 Platzer and Geoff Sutcliffe, editors, Conference on Automated Deduction (CADE), volume 12699 of Lecture Notes in Computer Science, pages 450\u2013467. Springer, 2021.","DOI":"10.1007\/978-3-030-79876-5_26"},{"key":"19_CR37","doi-asserted-by":"crossref","unstructured":"Aaron Stump, Duckki Oe, Andrew Reynolds, Liana Hadarean, and Cesare Tinelli. SMT proof checking using a logical framework. Formal Methods in System Design, 42(1):91\u2013118, 2013.","DOI":"10.1007\/s10703-012-0163-3"},{"key":"19_CR38","doi-asserted-by":"crossref","unstructured":"Dominik Winterer, Chengyu Zhang, and Zhendong Su. Validating SMT solvers via semantic fusion. In Alastair\u00a0F. Donaldson and Emina Torlak, editors, Conference on Programming Language Design and Implementation (PLDI), pages 718\u2013730. ACM, 2020.","DOI":"10.1145\/3385412.3385985"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-30823-9_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,19]],"date-time":"2024-10-19T00:20:32Z","timestamp":1729297232000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-30823-9_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031308222","9783031308239"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-30823-9_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"22 April 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","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":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 April 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 April 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2023\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"169","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"56","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}