{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T18:13:09Z","timestamp":1760033589679,"version":"build-2065373602"},"reference-count":77,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/T00021X\/1"],"award-info":[{"award-number":["EP\/T00021X\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101089343"],"award-info":[{"award-number":["101089343"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004359","name":"Swedish Research Council","doi-asserted-by":"crossref","award":["2021-06327"],"award-info":[{"award-number":["2021-06327"]}],"id":[{"id":"10.13039\/501100004359","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>The past decade has witnessed substantial developments in string solving.  \n Motivated by the complexity of string solving strategies adopted in existing  \n string solvers, we investigate a simple and generic method  \n for solving string constraints: regular constraint propagation.  \n The method repeatedly computes pre- or post-images of regular languages  \n under  \n the string functions present in a string formula, inferring more and more  \n knowledge about the possible values of string variables, until either a  \n conflict is found or satisfiability of the string formula can be  \n concluded. Such a propagation strategy is applicable to string constraints  \n with multiple operations like concatenation, replace, and almost all  \n flavors of string transductions. We demonstrate the generality and  \n effectiveness of  \n this method theoretically and experimentally.   \n On the theoretical side, we  \n show that RCP is sound and complete for a large fragment of string  \n constraints, subsuming both straight-line and chain-free constraints,  \n two of the most expressive decidable fragments for which some modern string solvers  \n provide formal completeness guarantees.  \n On the practical side, we implement regular constraint propagation within the open-source string solver OSTRICH.  \n Our experimental evaluation shows that this addition significantly improves OSTRICH\u2019s performance and makes it competitive with existing solvers. In fact, it substantially outperforms other solvers on random PCP and bioinformatics benchmarks. The results also suggest that incorporating regular constraint propagation alongside other techniques could lead to substantial performance gains for existing solvers.<\/jats:p>","DOI":"10.1145\/3763165","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:51:31Z","timestamp":1759999891000},"page":"3203-3231","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["The Power of Regular Constraint Propagation"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4913-3800","authenticated-orcid":false,"given":"Matthew","family":"Hague","sequence":"first","affiliation":[{"name":"Royal Holloway University of London, Egham, United Kingdom"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4321-3105","authenticated-orcid":false,"given":"Artur","family":"Je\u017c","sequence":"additional","affiliation":[{"name":"University of Wroclaw, Wroclaw, Poland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4715-5096","authenticated-orcid":false,"given":"Anthony Widjaja","family":"Lin","sequence":"additional","affiliation":[{"name":"RPTU Kaiserslautern-Landau, Kaiserslautern, Germany"},{"name":"MPI-SWS, Kaiserslautern, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4817-4563","authenticated-orcid":false,"given":"Oliver","family":"Markgraf","sequence":"additional","affiliation":[{"name":"RPTU Kaiserslautern-Landau, Kaiserslautern, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2733-7098","authenticated-orcid":false,"given":"Philipp","family":"R\u00fcmmer","sequence":"additional","affiliation":[{"name":"University of Regensburg, Regensburg, Germany"},{"name":"Uppsala University, Uppsala, Sweden"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"2013. OWASP: Top10. https:\/\/owasp.org\/www-pdf-archive\/OWASP_Top_10_-_2013.pdf"},{"key":"e_1_2_1_2_1","unstructured":"2017. OWASP: Top10. https:\/\/owasp.org\/www-project-top-ten\/2017\/"},{"key":"e_1_2_1_3_1","unstructured":"2021. OWASP: Top10. https:\/\/owasp.org\/Top10\/"},{"key":"e_1_2_1_4_1","volume-title":"19th International Satisfiability Modulo Theories Competition. https:\/\/smt-comp.github.io\/2024\/","year":"2024","unstructured":"2024. SMT-COMP 2024: The 19th International Satisfiability Modulo Theories Competition. https:\/\/smt-comp.github.io\/2024\/"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-89051-3_17"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8602997"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3140587.3062384"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_29"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_10"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31784-3_16"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2010.1"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22012-8_1"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3484198"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66158-2_1"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-61499-495-4-26"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","unstructured":"Haniel Barbosa Clark 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. 2022. cvc5: A Versatile and Industrial-Strength SMT Solver. 415\u2013442. isbn:978-3-030-99523-2 https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24 10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_4"},{"key":"e_1_2_1_18_1","unstructured":"Clark Barrett Pascal Fontaine and Cesare Tinelli. 2024. The SMT-LIB Standard: Version 2.6. http:\/\/smt-lib.org"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-663-09367-1"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2022.12.009"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","unstructured":"Murphy Berzish Vijay Ganesh and Yunhui Zheng. 2017. Z3str3: A String Solver with Theory-aware Heuristics. In 2017 Formal Methods in Computer Aided Design (FMCAD). 55\u201359. https:\/\/doi.org\/10.23919\/FMCAD.2017.8102241 10.23919\/FMCAD.2017.8102241","DOI":"10.23919\/FMCAD.2017.8102241"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_14"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_23"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_6"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18275-4_7"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158091"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498707"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-59152-6_18"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290362"},{"key":"e_1_2_1_30_1","volume-title":"Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Oliver Markgraf, Anthony W. Lin, Philipp Ruemmer, and Zhilin Wu.","author":"Chen Taolue","year":"2023","unstructured":"Taolue Chen, Riccardo De Masellis, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Oliver Markgraf, Anthony W. Lin, Philipp Ruemmer, and Zhilin Wu. 2023. OSTRICH Version 1.3. https:\/\/www.cs.rhul.ac.uk\/home\/uxac009\/files\/papers\/smtcomp2023.pdf"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-11194-0_12"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622872"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57246-3_2"},{"key":"e_1_2_1_34_1","volume-title":"Bioinformatics Algorithms: An Active Learning Approach","author":"Compeau Phillip","year":"2015","unstructured":"Phillip Compeau and Pavel Pevzner. 2015. Bioinformatics Algorithms: An Active Learning Approach, Volume 1 (2 ed.). Active Learning Publishers, La Jolla, CA. isbn:978-0990374619"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.1708.09073"},{"key":"e_1_2_1_36_1","volume-title":"Automatark automata benchmark","author":"D\u2019Antoni L","year":"2018","unstructured":"L D\u2019Antoni. 2018. Automatark automata benchmark (2018).. https:\/\/github.com\/lorisdanto\/automatark"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30806-3_8"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107326019.013"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201353"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45193-8_26"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","unstructured":"Matthew Hague Artur Je\u017c Anthony W. Lin Oliver Markgraf and Philipp R\u00fcmmer. 2025. The Power of Regular Constraint Propagation (Technical Report). arxiv:2508.19888. https:\/\/doi.org\/10.48550\/arXiv.2508.19888 10.48550\/arXiv.2508.19888","DOI":"10.48550\/arXiv.2508.19888"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SAT.2024.14"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/SYNASC.2017.00033"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158092"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2743014"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37703-7_2"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3497775.3503691"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2377656.2377662"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02768-1_19"},{"key":"e_1_2_1_51_1","volume-title":"ReDoSHunter: A Combined Static and Dynamic Approach for Regular Expression DoS Detection. In 30th USENIX Security Symposium (USENIX Security 21)","author":"Li Yeting","year":"2021","unstructured":"Yeting Li, Zixuan Chen, Jialun Cao, Zhiwu Xu, Qiancheng Peng, Haiming Chen, Liyuan Chen, and Shing-Chi Cheung. 2021. ReDoSHunter: A Combined Static and Dynamic Approach for Regular Expression DoS Detection. In 30th USENIX Security Symposium (USENIX Security 21). USENIX Association, 3847\u20133864. isbn:978-1-939133-24-3 https:\/\/www.usenix.org\/conference\/usenixsecurity21\/presentation\/li-yeting"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837641"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.46298\/LMCS-17(4:4)2021"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","unstructured":"Kevin Lotz Amit Goel Bruno Dutertre Benjamin Kiesl-Reiter Soonho Kong Rupak Majumdar and Dirk Nowotka. 2023. Solving String Constraints Using SAT. In Computer Aided Verification Constantin Enea and Akash Lal (Eds.). Springer Nature Switzerland Cham. 187\u2013208. isbn:978-3-031-37703-7 https:\/\/doi.org\/10.1007\/978-3-031-37703-7_9 10.1007\/978-3-031-37703-7_9","DOI":"10.1007\/978-3-031-37703-7_9"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2024\/211"},{"key":"e_1_2_1_56_1","volume-title":"Z3-alpha: A Reinforcement Learning Guided SMT Solver SMT-COMP","author":"Lu Zhengyang","year":"2023","unstructured":"Zhengyang Lu, Stefan Siemer, Piyush Jha, Florin Manea, Joel Day, and Vijay Ganesh. 2023. Z3-alpha: A Reinforcement Learning Guided SMT Solver SMT-COMP 2023. https:\/\/smt-comp.github.io\/2023\/system-descriptions\/z3-alpha.pdf"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1070\/SM1977V032N02ABEH002376"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","unstructured":"Oliver Markgraf Artur Je\u017c Matthew Hague Philipp R\u00fcmmer and Anthony Widjaja Lin. 2025. The Power of Regular Constraint Propagation. Artifact on Zenodo. https:\/\/doi.org\/10.5281\/zenodo.15805177 10.5281\/zenodo.15805177","DOI":"10.5281\/zenodo.15805177"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/1060745.1060809"},{"key":"e_1_2_1_60_1","unstructured":"Anders M\u00f8ller. 2021. dk.brics.automaton \u2013 Finite-State Automata and Regular Expressions for Java. https:\/\/www.brics.dk\/automaton"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-90870-6_21"},{"key":"e_1_2_1_62_1","volume-title":"Bioinformatics: Sequence and Genome Analysis (2 ed.)","author":"Mount David W.","year":"2004","unstructured":"David W. Mount. 2004. Bioinformatics: Sequence and Genome Analysis (2 ed.). Cold Spring Harbor Laboratory Press, Cold Spring Harbor, NY. isbn:978-0879697129"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01457113"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-24258-9_20"},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/301250.301443"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.11061097"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_24"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.5555\/2843512"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.38"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-59776-8_5"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454066"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/2522920.2522926"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238189"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_13"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_13"},{"key":"e_1_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_14"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491456"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763165","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:45:02Z","timestamp":1760031902000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763165"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":77,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763165"],"URL":"https:\/\/doi.org\/10.1145\/3763165","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-26","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}