{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,19]],"date-time":"2026-03-19T02:25:28Z","timestamp":1773887128743,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":45,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T00:00:00Z","timestamp":1736467200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"NSF (National Science Foundation)","award":["2319572"],"award-info":[{"award-number":["2319572"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,1,10]]},"DOI":"10.1145\/3703595.3705884","type":"proceedings-article","created":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T21:23:16Z","timestamp":1736544196000},"page":"198-213","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Verified and Efficient Matching of Regular Expressions with Lookaround"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0007-0462-8080","authenticated-orcid":false,"given":"Agnishom","family":"Chattopadhyay","sequence":"first","affiliation":[{"name":"Rice University, Houston, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4523-3401","authenticated-orcid":false,"given":"Angela W.","family":"Li","sequence":"additional","affiliation":[{"name":"Rice University, Houston, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1209-7738","authenticated-orcid":false,"given":"Konstantinos","family":"Mamouras","sequence":"additional","affiliation":[{"name":"Rice University, Houston, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,1,10]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00182-4"},{"key":"e_1_3_2_2_2_1","volume-title":"Program Analysis and Verification Based on Kleene Algebra in Isabelle\/HOL","author":"Armstrong Alasdair","unstructured":"Alasdair Armstrong, Georg Struth, and Tjark Weber. 2013. Program Analysis and Verification Based on Kleene Algebra in Isabelle\/HOL. In Interactive Theorem Proving, Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 197\u2013212. isbn:978-3-642-39634-2"},{"key":"e_1_3_2_2_3_1","volume-title":"A Compact Proof of Decidability for Regular Expression Equivalence","author":"Asperti Andrea","unstructured":"Andrea Asperti. 2012. A Compact Proof of Decidability for Regular Expression Equivalence. In Interactive Theorem Proving, Lennart Beringer and Amy Felty (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 283\u2013298. isbn:978-3-642-32347-8"},{"key":"e_1_3_2_2_4_1","volume-title":"Claudio Sacerdoti Coen, and Enrico Tassi","author":"Asperti Andrea","year":"2010","unstructured":"Andrea Asperti, Claudio Sacerdoti Coen, and Enrico Tassi. 2010. Regular Expressions, au point. arxiv:1010.2604."},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656431"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.151.7"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.3897\/jucs.66330"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_13"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/321239.321249"},{"key":"e_1_3_2_2_10_1","unstructured":"Agnishom Chattopadhyay. 2024. Efficient Matching of Regular Expressions with Lookaround - Coq Source Code. https:\/\/github.com\/Agnishom\/lregex\/"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_11"},{"key":"e_1_3_2_2_12_1","unstructured":"Russ Cox. 2010. Regular Expression Matching in the Wild. https:\/\/swtch.com\/ rsc\/regexp\/regexp3.html"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236027"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00032"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674666"},{"key":"e_1_3_2_2_16_1","volume-title":"A Constructive Theory of Regular Languages in Coq","author":"Doczkal Christian","unstructured":"Christian Doczkal, Jan-Oliver Kaiser, and Gert Smolka. 2013. A Constructive Theory of Regular Languages in Coq. In Certified Programs and Proofs, Georges Gonthier and Michael Norrish (Eds.). Springer International Publishing, Cham. 82\u201397. isbn:978-3-319-03545-1"},{"key":"e_1_3_2_2_17_1","volume-title":"Two-Way Automata in Coq","author":"Doczkal Christian","unstructured":"Christian Doczkal and Gert Smolka. 2016. Two-Way Automata in Coq. In Interactive Theorem Proving, Jasmin Christian Blanchette and Stephan Merz (Eds.). Springer International Publishing, Cham. 151\u2013166. isbn:978-3-319-43144-4"},{"key":"e_1_3_2_2_18_1","volume-title":"Certified Parsing of Regular Languages","author":"Firsov Denis","unstructured":"Denis Firsov and Tarmo Uustalu. 2013. Certified Parsing of Regular Languages. In Certified Programs and Proofs, Georges Gonthier and Michael Norrish (Eds.). Springer International Publishing, Cham. 98\u2013113. isbn:978-3-319-03545-1"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863594"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27836-8_53"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57267-8_4"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837647"},{"key":"e_1_3_2_2_23_1","unstructured":"2023. Intel\u2019s Hyperscan: A high-performance multiple regex matching library. https:\/\/github.com\/intel\/hyperscan"},{"key":"e_1_3_2_2_24_1","unstructured":"Ohad Kammar and Katarzyna Marek. 2023. Idris TyRE: a dependently typed regex parser. arxiv:2305.04480."},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(69)80027-9"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103776.2103784"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1037"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/256167.256195"},{"key":"e_1_3_2_2_29_1","unstructured":"Dexter Kozen. 2001. Automata on Guarded Strings and Applications. USA."},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586044"},{"key":"e_1_3_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632934"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656461"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33314-9_7"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591262"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-21254-3_32"},{"key":"e_1_3_2_2_36_1","volume-title":"Unified Decision Procedures for Regular Expression Equivalence","author":"Nipkow Tobias","unstructured":"Tobias Nipkow and Dmitriy Traytel. 2014. Unified Decision Procedures for Regular Expression Equivalence. In Interactive Theorem Proving, Gerwin Klein and Ruben Gamboa (Eds.). Springer International Publishing, Cham. 450\u2013466. isbn:978-3-319-08970-6"},{"key":"e_1_3_2_2_37_1","volume-title":"d.]. Java Regex Matching. https:\/\/docs.oracle.com\/javase\/8\/docs\/api\/java\/util\/regex\/Pattern.html [Online","year":"2024","unstructured":"Oracle. [n. d.]. Java Regex Matching. https:\/\/docs.oracle.com\/javase\/8\/docs\/api\/java\/util\/regex\/Pattern.html [Online; accessed Feb 28, 2024]"},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.4380171105"},{"key":"e_1_3_2_2_39_1","volume-title":"Kleene Algebra with Tests and Coq Tools for while Programs","author":"Pous Damien","unstructured":"Damien Pous. 2013. Kleene Algebra with Tests and Coq Tools for while Programs. In Interactive Theorem Proving, Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 180\u2013196. isbn:978-3-642-39634-2"},{"key":"e_1_3_2_2_40_1","unstructured":"2023. RE2: Google\u2019s regular expression library. https:\/\/github.com\/google\/re2"},{"key":"e_1_3_2_2_41_1","volume-title":"https:\/\/coq.inria.fr\/doc\/V8.19.2\/refman\/addendum\/generalized-rewriting.html [Online","author":"Sozeau Matthieu","year":"2024","unstructured":"Matthieu Sozeau. 2023. Generalized Rewriting. https:\/\/coq.inria.fr\/doc\/V8.19.2\/refman\/addendum\/generalized-rewriting.html [Online; accessed Aug 7, 2024]"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454066"},{"key":"e_1_3_2_2_43_1","volume-title":"Perl-compatible Regular Expressions (revised API: PCRE2). https:\/\/pcre2project.github.io\/pcre2\/doc\/html\/index.html [Online","author":"Developers The","year":"2023","unstructured":"The PCRE2 Developers. 2022. Perl-compatible Regular Expressions (revised API: PCRE2). https:\/\/pcre2project.github.io\/pcre2\/doc\/html\/index.html [Online; accessed Feb 26, 2023]"},{"key":"e_1_3_2_2_44_1","unstructured":"Ian Erik Varatalu Margus Veanes and Juhan-Peep Ernits. 2023. Derivative Based Extended Regular Expression Matching Supporting Intersection Complement and Lookarounds. arxiv:2309.14401."},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3636501.3636959"}],"event":{"name":"CPP '25: 14th ACM SIGPLAN International Conference on Certified Programs and Proofs","location":"Denver CO USA","acronym":"CPP '25","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG"]},"container-title":["Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3703595.3705884","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3703595.3705884","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:18:08Z","timestamp":1750295888000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3703595.3705884"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,10]]},"references-count":45,"alternative-id":["10.1145\/3703595.3705884","10.1145\/3703595"],"URL":"https:\/\/doi.org\/10.1145\/3703595.3705884","relation":{},"subject":[],"published":{"date-parts":[[2025,1,10]]},"assertion":[{"value":"2025-01-10","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}