{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T10:22:48Z","timestamp":1779099768159,"version":"3.51.4"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"10","license":[{"start":{"date-parts":[[2023,9,22]],"date-time":"2023-09-22T00:00:00Z","timestamp":1695340800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Commun. ACM"],"published-print":{"date-parts":[[2023,10]]},"abstract":"<jats:p>Moving toward a full suite of proof-producing automated reasoning tools with SMT solvers that can produce full, independently checkable proofs for real-world problems.<\/jats:p>","DOI":"10.1145\/3587692","type":"journal-article","created":{"date-parts":[[2023,9,22]],"date-time":"2023-09-22T15:28:35Z","timestamp":1695396515000},"page":"86-95","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["Generating and Exploiting Automated Reasoning Proof Certificates"],"prefix":"10.1145","volume":"66","author":[{"given":"Haniel","family":"Barbosa","sequence":"first","affiliation":[{"name":"Universidade Federal de Minas Gerais, Belo Horizonte, Brazil"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[{"name":"Stanford University, Stanford, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Byron","family":"Cook","sequence":"additional","affiliation":[{"name":"Amazon, New York, NY, USA and University College London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bruno","family":"Dutertre","sequence":"additional","affiliation":[{"name":"Amazon, New York, NY, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gereon","family":"Kremer","sequence":"additional","affiliation":[{"name":"Stanford University, Stanford, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hanna","family":"Lachnitt","sequence":"additional","affiliation":[{"name":"Stanford University, Stanford, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aina","family":"Niemetz","sequence":"additional","affiliation":[{"name":"Stanford University, Stanford, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andres","family":"N\u00f6tzli","sequence":"additional","affiliation":[{"name":"Stanford University, Stanford, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alex","family":"Ozdemir","sequence":"additional","affiliation":[{"name":"Stanford University, Stanford, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mathias","family":"Preiner","sequence":"additional","affiliation":[{"name":"Stanford University, Stanford, CA, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Reynolds","sequence":"additional","affiliation":[{"name":"The University of Iowa, Iowa City, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[{"name":"The University of Iowa, Iowa City, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yoni","family":"Zohar","sequence":"additional","affiliation":[{"name":"Bar-Ilan University, Ramat Gan, Israel"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,9,22]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the 33rd Intern. Conf. on Computer-Aided Verification (2021)","author":"Amrutesh K.","unstructured":"Amrutesh K. and Cook, B. How I learned to stop worrying and start applying automated reasoning. In Proceedings of the 33rd Intern. Conf. on Computer-Aided Verification (2021); https:\/\/bit.ly\/3QO7vLt."},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30823-9_19"},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","unstructured":"Backes J. et al. Semantic-based automated reasoning for AWS access policies using SMT. 2018 Formal Methods in Computer Aided Design 1--9.","DOI":"10.23919\/FMCAD.2018.8602994"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72016-2_4"},{"key":"e_1_2_1_5_1","first-page":"3","article-title":"A survey of symbolic execution techniques","volume":"51","author":"Baldoni R.","year":"2018","unstructured":"Baldoni, R. et al. A survey of symbolic execution techniques. ACM Computing Surveys 51, 3 (2018), 50:1--50:39.","journal-title":"ACM Computing Surveys"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the 28th Intern. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, D. Fisman and G. Rosu (Eds.)","author":"Barbosa H.","year":"2022","unstructured":"Barbosa, H. et al. &lt;code&gt;cvc5&lt;\/code&gt;: A versatile and industrial-strength SMT solver. In Proceedings of the 28th Intern. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, D. Fisman and G. Rosu (Eds.), Springer (2022), 415--442."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-09502-y"},{"key":"e_1_2_1_8_1","volume-title":"Pattinson (Eds.) In Proceedings of the 11th Intern. Joint Conf. on Automated Reasoning. Springer","author":"Barbosa H.","year":"2022","unstructured":"Barbosa, H. et al. Flexible proof production in an industrial-strength SMT solver. J. Blanchette, L. Kov\u00e1cs, and D. Pattinson (Eds.) In Proceedings of the 11th Intern. Joint Conf. on Automated Reasoning. Springer (2022), 15--35."},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 23rd Intern. Conf. on Computer Aided Verification, G. Gopalakrishnan and S. Qadeer (Eds.), Springer (July","author":"Barrett C.W.","year":"2011","unstructured":"Barrett, C.W. et al. &lt;code&gt;CVC4&lt;\/code&gt;. In Proceedings of the 23rd Intern. Conf. on Computer Aided Verification, G. Gopalakrishnan and S. Qadeer (Eds.), Springer (July 2011), 171--177."},{"key":"e_1_2_1_10_1","volume-title":"Satisfiability modulo theories. Handbook of Satisfiability---","author":"Barrett C.W.","year":"2021","unstructured":"Barrett, C.W. Satisfiability modulo theories. Handbook of Satisfiability---2nd Edition. A. Biere, M. Heule, H. van Maaren, and T. Walsh, (Eds.), IOS Press (2021), 1267--1329.","edition":"2"},{"key":"e_1_2_1_11_1","volume-title":"Satisfiability modulo theories. Handbook of Model Checking","author":"Barrett C.W.","year":"2018","unstructured":"Barrett, C.W. and Tinelli, C. Satisfiability modulo theories. Handbook of Model Checking, E.M. Clarke, T.A. Henzinger, H. Veith, and R. Bloem (Eds.), Springer (2018), 305--343."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9278-5"},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the 22nd Intern. Conf. on Automated Deduction, R.A. Schmidt, (Ed.), Springer (Aug.","author":"Bouton T.","year":"2009","unstructured":"Bouton, T. et al. verit: An open, trustable and efficient smt-solver. In Proceedings of the 22nd Intern. Conf. on Automated Deduction, R.A. Schmidt, (Ed.), Springer (Aug. 2009), 151--156."},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the 11th Intern. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, N. Halbwachs and L.D. Zuck, (Eds.), Springer (Apr.","author":"Bozzano M.","year":"2005","unstructured":"Bozzano, M. et al. An incremental and layered procedure for the satisfiability of linear arithmetic logic. In Proceedings of the 11th Intern. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, N. Halbwachs and L.D. Zuck, (Eds.), Springer (Apr. 2005), 317--333."},{"key":"e_1_2_1_15_1","volume-title":"The Calculus of Computation---Decision Procedures With Applications to Verification","author":"Bradley A.R.","year":"2007","unstructured":"Bradley, A.R. and Manna, Z. The Calculus of Computation---Decision Procedures With Applications to Verification, Springer (2007)."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31759-0_19"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of the 28th Intern. Conf. on Automated Deduction, L. de Moura (Ed.), Springer (Aug.","author":"Cruz-Filipe L.","year":"2017","unstructured":"Cruz-Filipe, L. et al. Efficient certified RAT verification. In Proceedings of the 28th Intern. Conf. on Automated Deduction, L. de Moura (Ed.), Springer (Aug. 2017), 220--236."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the LPAR 2008 Workshops","author":"de Moura L.M.","year":"2008","unstructured":"de Moura, L.M. and Bj\u00f8rner, N.S. Proofs and refutations, and Z3. In Proceedings of the LPAR 2008 Workshops, Knowledge Exchange: Automated Provers and Proof Assistants and the 7th Intern. Workshop on the Implementation of Logics, P. Rudnicki, G. Sutcliffe, B. Konev, R.A. Schmidt, and S. Schulz (Eds.), (Nov. 2008)."},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the 6th Intern. Conf. on Theory and Applications of Satisfiability Testing, E. Giunchiglia and A. Tacchella (Eds.), Springer (May","author":"E\u00e9n N.","year":"2003","unstructured":"E\u00e9n, N. and S\u00f6rensson, N. An extensible sat-solver. In Proceedings of the 6th Intern. Conf. on Theory and Applications of Satisfiability Testing, E. Giunchiglia and A. Tacchella (Eds.), Springer (May 2003), 502--518."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_7"},{"key":"e_1_2_1_22_1","volume-title":"Proceedings 8th Intern. Conf. on Interactive Theorem Proving, M. Ayala-Rinc\u00f3n and C.A. Mu\u00f1oz (Eds.), Springer (Sept.","author":"Heule M.","year":"2017","unstructured":"Heule, M. et al. Efficient, verified checking of propositional proofs. In Proceedings 8th Intern. Conf. on Interactive Theorem Proving, M. Ayala-Rinc\u00f3n and C.A. Mu\u00f1oz (Eds.), Springer (Sept. 2017), 269--284."},{"key":"e_1_2_1_23_1","volume-title":"The DRAT format and drat-trim checker. CoRR, abs\/1610.06229","author":"Heule M.J.H.","year":"2016","unstructured":"Heule, M.J.H. The DRAT format and drat-trim checker. CoRR, abs\/1610.06229, 2016."},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the 2016 Formal Methods in Computer-Aided Design, R. Piskac and M. Talupur (Eds.), IEEE, 93--100","author":"Katz G.","unstructured":"Katz, G. et al. Lazy proofs for DPLL(T)-based SMT solvers. In Proceedings of the 2016 Formal Methods in Computer-Aided Design, R. Piskac and M. Talupur (Eds.), IEEE, 93--100."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94205-6_34"},{"key":"e_1_2_1_26_1","first-page":"4","article-title":"(Eds.): Handbook of model checking","volume":"31","author":"Konnov I.","year":"2019","unstructured":"Konnov, I. et al. (Eds.): Handbook of model checking. In Proceedings of Formal Aspects of Computing 31, 4, Springer (2019), 455--456.","journal-title":"Proceedings of Formal Aspects of Computing"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the 26th Intern. Conf. on Automated Deduction, L. de Moura (Ed.), Springer (Aug.","author":"Lammich P.","year":"2017","unstructured":"Lammich, P. Efficient verified (UN)SAT certificate checking. In Proceedings of the 26th Intern. Conf. on Automated Deduction, L. de Moura (Ed.), Springer (Aug. 2017), 237--254."},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the 26th Computer Aided Verification Intern. Conf., A. Biere and R. Bloem, (Eds.), Springer (July","author":"Liang T.","year":"2014","unstructured":"Liang, T. et al. A DPLL(T) theory solver for a theory of strings and regular expressions. In Proceedings of the 26th Computer Aided Verification Intern. Conf., A. Biere and R. Bloem, (Eds.), Springer (July 2014), 646--662."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_33"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217856.1217859"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the 2022 Formal Methods in Computer Aided Design, IEEE, 65--74","author":"N\u00f6tzli A.","unstructured":"N\u00f6tzli, A. et al. Reconstructing fine-grained proofs of rewrites using a domain-specific language. In Proceedings of the 2022 Formal Methods in Computer Aided Design, IEEE, 65--74."},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the 2020 Formal Methods in Computer Aided Design, IEEE, 225--235","author":"Reynolds A.","unstructured":"Reynolds, A. et al. Reductions for strings and regular expressions revisited. In Proceedings of the 2020 Formal Methods in Computer Aided Design, IEEE, 225--235."},{"key":"e_1_2_1_34_1","volume-title":"Proceedings of the 29th Computer Aided Verification Intern. Conf., R. Majumdar and V. Kuncak, (Eds.), Springer (July","author":"Reynolds A.","year":"2017","unstructured":"Reynolds, A. et al. Scaling up DPLL(T) string solvers using context-dependent simplification. In Proceedings of the 29th Computer Aided Verification Intern. Conf., R. Majumdar and V. Kuncak, (Eds.), Springer (July 2017), 453--474."},{"key":"e_1_2_1_35_1","volume-title":"Handbook of Automated Reasoning (in 2 Volumes)","author":"Robinson J.A.","year":"2001","unstructured":"Robinson, J.A. and Voronkov, A. Preface. Handbook of Automated Reasoning (in 2 Volumes), Elsevier and MIT Press (2001), v--vii."},{"key":"e_1_2_1_36_1","doi-asserted-by":"crossref","unstructured":"Schurr H-J. et al. Alethe: Towards a generic SMT proof format (extended abstract) (2021) 336:49--54.","DOI":"10.4204\/EPTCS.336.6"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592437"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706337"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0163-3"},{"key":"e_1_2_1_40_1","unstructured":"The Coq development team. The coq proof assistant reference manual version 8.9 (2019)."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-57288-8_29"}],"container-title":["Communications of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3587692","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3587692","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:07:59Z","timestamp":1750183679000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3587692"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,22]]},"references-count":41,"journal-issue":{"issue":"10","published-print":{"date-parts":[[2023,10]]}},"alternative-id":["10.1145\/3587692"],"URL":"https:\/\/doi.org\/10.1145\/3587692","relation":{},"ISSN":["0001-0782","1557-7317"],"issn-type":[{"value":"0001-0782","type":"print"},{"value":"1557-7317","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,9,22]]},"assertion":[{"value":"2023-09-22","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}