{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T11:00:42Z","timestamp":1784804442373,"version":"3.55.0"},"publisher-location":"Cham","reference-count":12,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032325884","type":"print"},{"value":"9783032325891","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>cvc5 is a state-of-the-art proof-producing SMT solver, capable of solving formulas over a myriad of theories, including Unicode strings. Matching regular expressions against concrete strings is done numerous times during the solving process, and forms a bottleneck in proof-checking for unsatisfiable formulas. We describe three approaches for checking regular expressions in the Eunoia proof-checking framework, and evaluate them on proofs produced by cvc5.<\/jats:p>","DOI":"10.1007\/978-3-032-32589-1_16","type":"book-chapter","created":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T10:02:16Z","timestamp":1784800936000},"page":"267-275","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Checking Regular Expressions in\u00a0Cvc5 Proofs"],"prefix":"10.1007","author":[{"given":"Ofec","family":"Israel","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Yoni","family":"Zohar","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Andrew","family":"Reynolds","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"S.","family":"Hitarth","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Bruno","family":"Dutertre","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2026,7,24]]},"reference":[{"key":"16_CR1","doi-asserted-by":"crossref","unstructured":"Andreotti, B., Lachnitt, H., Barbosa, H.: \u201cCarcara: an efficient proof checker and elaborator for SMT proofs in the Alethe format. In: TACAS (1), vol. 13993. LNCS. Springer, pp. 367\u2013386 (2023)","DOI":"10.1007\/978-3-031-30823-9_19"},{"key":"16_CR2","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: CVC5: a versatile and industrial-strength SMT solver. Presented at the (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"16_CR3","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2016)"},{"key":"16_CR4","doi-asserted-by":"crossref","unstructured":"Barrett, C., et al.: \u201cSatisfiability modulo theories\u201d. In: Handbook of Satisfiability, Second Edition. Vol. 336. Frontiers in Artificial Intelligence and Applications. IOS Press. Chap. 33, pp. 825\u2013885 (2021)","DOI":"10.3233\/FAIA201017"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"Brzozowski, J.A.: \u201cDerivatives of regular expressions\u201d. J. ACM 11(4), 481\u2013494 (1964)","DOI":"10.1145\/321239.321249"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Owens, S., Reppy, J.H., Turon, A.: \u201cRegular-expression derivatives re-examined\u201d. In: J. Funct. Program. 19(2), 173\u2013190 (2009)","DOI":"10.1017\/S0956796808007090"},{"key":"16_CR7","unstructured":"Preiner, M.: SMT-LIB release 2024 (non-incremental benchmarks) (2024)"},{"key":"16_CR8","unstructured":"Reynolds, A., et al.: \u201cEthos: a fast proof checker for the eunoia logical framework\u201d. In: Automated Reasoning - 13th International Joint Conference, IJCAR 2026. Ed. by Armin Biere, Carsten Lutz, and Sara Negri. Lecture Notes in Computer Science. Springer ( 2026)"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Reynolds, A., et al.: \u201cThe cooperating proof calculus: comprehensive proofs for an SMT solver\u201d. In: CAV. LNCS. To appear. Springer (2026)","DOI":"10.1007\/978-3-032-32526-6_9"},{"key":"16_CR10","unstructured":"The Ethos Manual. https:\/\/github.com\/cvc5\/ethos\/blob\/main\/usermanual.md (2025)"},{"key":"16_CR11","doi-asserted-by":"crossref","unstructured":"Thompson, K.: \u201cRegular expression search algorithm\u201d. Commun. ACM 11(6), 419\u2013422 (1968)","DOI":"10.1145\/363347.363387"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Varatalu, I.E., et al.: \u201cRegex decision procedures in extended RE#\u201d. In: CAV. Springer, pp. 106\u2013129 (2025)","DOI":"10.1007\/978-3-031-98682-6_7"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-32589-1_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T10:02:19Z","timestamp":1784800939000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-32589-1_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032325884","9783032325891"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-32589-1_16","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":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","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":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.floc26.org\/ijcar","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}