{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,8]],"date-time":"2026-10-08T11:34:17Z","timestamp":1791459257307,"version":"4.3.4"},"reference-count":60,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T00:00:00Z","timestamp":1641945600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,1,16]]},"abstract":"<jats:p>Regular expressions are a classical concept in formal language theory. Regular expressions in programming languages (RegEx) such as JavaScript, feature non-standard semantics of operators (e.g. greedy\/lazy Kleene star), as well as additional features such as capturing groups and references. While symbolic execution of programs containing RegExes appeals to string solvers natively supporting important features of RegEx, such a string solver is hitherto missing. In this paper, we propose the first string theory and string solver that natively provides such support. The key idea of our string solver is to introduce a new automata model, called prioritized streaming string transducers (PSST), to formalize the semantics of RegEx-dependent string functions. PSSTs combine priorities, which have previously been introduced in prioritized finite-state automata to capture greedy\/lazy semantics, with string variables as in streaming string transducers to model capturing groups. We validate the consistency of the formal semantics with the actual JavaScript semantics by extensive experiments. Furthermore, to solve the string constraints, we show that PSSTs enjoy nice closure and algorithmic properties, in particular, the regularity-preserving property (i.e., pre-images of regular constraints under PSSTs are regular), and introduce a sound sequent calculus that exploits these properties and performs propagation of regular constraints by means of taking post-images or pre-images. Although the satisfiability of the string constraint language is generally undecidable, we show that our approach is complete for the so-called straight-line fragment. We evaluate the performance of our string solver on over 195000 string constraints generated from an open-source RegEx library. The experimental results show the efficacy of our approach, drastically improving the existing methods (via symbolic execution) in both precision and efficiency.<\/jats:p>","DOI":"10.1145\/3498707","type":"journal-article","created":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T17:03:12Z","timestamp":1642006992000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":39,"title":["Solving string constraints with Regex-dependent functions through transducers with priorities and variables"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5993-1665","authenticated-orcid":false,"given":"Taolue","family":"Chen","sequence":"first","affiliation":[{"name":"Birkbeck University of London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alejandro","family":"Flores-Lamas","sequence":"additional","affiliation":[{"name":"Royal Holloway University of London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4913-3800","authenticated-orcid":false,"given":"Matthew","family":"Hague","sequence":"additional","affiliation":[{"name":"Royal Holloway University of London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9171-4997","authenticated-orcid":false,"given":"Zhilei","family":"Han","sequence":"additional","affiliation":[{"name":"Tsinghua University, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Denghang","family":"Hu","sequence":"additional","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, China \/ University of Chinese Academy of Sciences, China"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shuanglong","family":"Kan","sequence":"additional","affiliation":[{"name":"TU Kaiserslautern, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4715-5096","authenticated-orcid":false,"given":"Anthony W.","family":"Lin","sequence":"additional","affiliation":[{"name":"TU Kaiserslautern, Germany \/ MPI-SWS, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2733-7098","authenticated-orcid":false,"given":"Philipp","family":"R\u00fcmmer","sequence":"additional","affiliation":[{"name":"Uppsala University, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0899-628X","authenticated-orcid":false,"given":"Zhilin","family":"Wu","sequence":"additional","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, China \/ University of Chinese Academy of Sciences, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,1,12]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062384"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8602997"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_10"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-31784-3_16"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSTTCS.2010.1"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22012-8_1"},{"key":"e_1_2_2_7_1","volume-title":"A Survey on String Constraint Solving. CoRR, abs\/2002.02376","author":"Amadini Roberto","year":"2020","unstructured":"Roberto Amadini . 2020. A Survey on String Constraint Solving. CoRR, abs\/2002.02376 ( 2020 ), arxiv:2002.02376. arxiv:2002.02376 Roberto Amadini. 2020. A Survey on String Constraint Solving. CoRR, abs\/2002.02376 (2020), arxiv:2002.02376. arxiv:2002.02376"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-19212-9_1"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66158-2_1"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.151.7"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.09.006"},{"key":"e_1_2_2_12_1","volume-title":"Proceedings of the Prague Stringology Conference 2017","author":"Berglund Martin","year":"2017","unstructured":"Martin Berglund and Brink van der Merwe. 2017. Regular Expressions with Backreferences Re-examined . In Proceedings of the Prague Stringology Conference 2017 , Prague, Czech Republic , August 28-30, 2017 , Jan Holub and Jan Zd\u00e1rek (Eds.). Department of Theoretical Computer Science, Faculty of Information Technology, Czech Technical University in Prague, 30\u201341. http:\/\/www.stringology.org\/event\/2017\/p04.html Martin Berglund and Brink van der Merwe. 2017. Regular Expressions with Backreferences Re-examined. In Proceedings of the Prague Stringology Conference 2017, Prague, Czech Republic, August 28-30, 2017, Jan Holub and Jan Zd\u00e1rek (Eds.). Department of Theoretical Computer Science, Faculty of Information Technology, Czech Technical University in Prague, 30\u201341. http:\/\/www.stringology.org\/event\/2017\/p04.html"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102241"},{"key":"e_1_2_2_14_1","unstructured":"Berzish Murphy. 2021. Z3str4: A Solver for Theories over Strings. Ph. D. Dissertation. http:\/\/hdl.handle.net\/10012\/17102  Berzish Murphy. 2021. Z3str4: A Solver for Theories over Strings. Ph. D. Dissertation. http:\/\/hdl.handle.net\/10012\/17102"},{"key":"e_1_2_2_15_1","unstructured":"Diep Bui and contributors. 2019. Z3-Trau. https:\/\/github.com\/diepbp\/z3-trau  Diep Bui and contributors. 2019. Z3-Trau. https:\/\/github.com\/diepbp\/z3-trau"},{"key":"e_1_2_2_16_1","unstructured":"Tevfik Bultan and contributors. 2015. ABC string solver. https:\/\/github.com\/vlab-cs-ucsb\/ABC  Tevfik Bultan and contributors. 2015. ABC string solver. https:\/\/github.com\/vlab-cs-ucsb\/ABC"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1142\/S012905410300214X"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00982-2_24"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1051\/ita:2006005"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/322234.322243"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158091"},{"key":"e_1_2_2_22_1","volume-title":"Philipp R\u00fcmmer, and Zhilin Wu.","author":"Chen Taolue","year":"2021","unstructured":"Taolue Chen , Alejandro Flores-Lamas , Matthew Hague , Zhilei Han , Denghang Hu , Shuanglong Kan , Anthony Widjaja Lin , Philipp R\u00fcmmer, and Zhilin Wu. 2021 . Solving String Constraints With Regex-Dependent Functions Through Transducers With Priorities And Variables. CoRR , abs\/2111.04298 (2021), arXiv:2111.04298. arxiv:2111.04298 Taolue Chen, Alejandro Flores-Lamas, Matthew Hague, Zhilei Han, Denghang Hu, Shuanglong Kan, Anthony Widjaja Lin, Philipp R\u00fcmmer, and Zhilin Wu. 2021. Solving String Constraints With Regex-Dependent Functions Through Transducers With Priorities And Variables. CoRR, abs\/2111.04298 (2021), arXiv:2111.04298. arxiv:2111.04298"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290362"},{"key":"e_1_2_2_24_1","unstructured":"Arlen Cox and Jason Leasure. 2017. Model Checking Regular Language Constraints. arxiv:1708.09073. arxiv:1708.09073  Arlen Cox and Jason Leasure. 2017. Model Checking Regular Language Constraints. arxiv:1708.09073. arxiv:1708.09073"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338906.3338909"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90015-T"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-012-9389-0"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2019.04.001"},{"key":"e_1_2_2_30_1","volume-title":"Linear Arithmetic over Length, and String-Number Conversion. CoRR, abs\/1605.09442","author":"Ganesh Vijay","year":"2016","unstructured":"Vijay Ganesh and Murphy Berzish . 2016. Undecidability of a Theory of Strings , Linear Arithmetic over Length, and String-Number Conversion. CoRR, abs\/1605.09442 ( 2016 ), arxiv:1605.09442 Vijay Ganesh and Murphy Berzish. 2016. Undecidability of a Theory of Strings, Linear Arithmetic over Length, and String-Number Conversion. CoRR, abs\/1605.09442 (2016), arxiv:1605.09442"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39611-3_21"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201353"},{"key":"e_1_2_2_33_1","volume-title":"Handbook of Practical Logic and Automated Reasoning","author":"Harrison John","unstructured":"John Harrison . 2009. Handbook of Practical Logic and Automated Reasoning . Cambridge University Press . isbn:978-0-521-89957-4 John Harrison. 2009. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press. isbn:978-0-521-89957-4"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158092"},{"key":"e_1_2_2_35_1","volume-title":"Fast and Precise Sanitizer Analysis with BEK. In USENIX Security Symposium. http:\/\/static.usenix.org\/events\/sec11\/tech\/full_papers\/Hooimeijer.pdf","author":"Hooimeijer Pieter","year":"2011","unstructured":"Pieter Hooimeijer , Benjamin Livshits , David Molnar , Prateek Saxena , and Margus Veanes . 2011 . Fast and Precise Sanitizer Analysis with BEK. In USENIX Security Symposium. http:\/\/static.usenix.org\/events\/sec11\/tech\/full_papers\/Hooimeijer.pdf Pieter Hooimeijer, Benjamin Livshits, David Molnar, Prateek Saxena, and Margus Veanes. 2011. Fast and Precise Sanitizer Analysis with BEK. In USENIX Security Symposium. http:\/\/static.usenix.org\/events\/sec11\/tech\/full_papers\/Hooimeijer.pdf"},{"key":"e_1_2_2_36_1","volume-title":"Ullman","author":"Hopcroft John E.","year":"1979","unstructured":"John E. Hopcroft and Jeffrey D . Ullman . 1979 . Introduction to Automata Theory, Languages and Computation. Addison-Wesley . John E. Hopcroft and Jeffrey D. Ullman. 1979. Introduction to Automata Theory, Languages and Computation. Addison-Wesley."},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2377656.2377662"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02768-1_19"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_43"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837641"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3092282.3092295"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314645"},{"key":"e_1_2_2_43_1","first-page":"55","article-title":"Multilevel magazine automata","volume":"12","author":"Masilov A. N.","year":"1976","unstructured":"A. N. Masilov . 1976 . Multilevel magazine automata . Probl. Peredachi Inf. , 12 , 1 (1976), 55 \u2013 62 . issn:0555-2923 A. N. Masilov. 1976. Multilevel magazine automata. Probl. Peredachi Inf., 12, 1 (1976), 55\u201362. issn:0555-2923","journal-title":"Probl. Peredachi Inf."},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2019.00047"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1217856.1217859"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.38"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2016.02.003"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-59776-8_5"},{"key":"e_1_2_2_49_1","volume-title":"Proceedings of the 27th USENIX Conference on Security Symposium (SEC\u201918)","author":"Staicu Cristian-Alexandru","year":"2018","unstructured":"Cristian-Alexandru Staicu and Michael Pradel . 2018 . Freezing the Web: A Study of ReDoS Vulnerabilities in Javascript-Based Web Servers . In Proceedings of the 27th USENIX Conference on Security Symposium (SEC\u201918) . USENIX Association, USA. 361\u2013376. https:\/\/www.usenix.org\/conference\/usenixsecurity18\/presentation\/staicu Cristian-Alexandru Staicu and Michael Pradel. 2018. Freezing the Web: A Study of ReDoS Vulnerabilities in Javascript-Based Web Servers. In Proceedings of the 27th USENIX Conference on Security Symposium (SEC\u201918). USENIX Association, USA. 361\u2013376. https:\/\/www.usenix.org\/conference\/usenixsecurity18\/presentation\/staicu"},{"key":"e_1_2_2_50_1","volume-title":"The Collected Papers of Gerhard Gentzen","unstructured":"1969. The Collected Papers of Gerhard Gentzen , M. E. Szabo (Ed.). North-Holland , Amsterdam . 1969. The Collected Papers of Gerhard Gentzen, M. E. Szabo (Ed.). North-Holland, Amsterdam."},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/363347.363387"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660372"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_12"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238189"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_13"},{"key":"e_1_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-013-0189-1"},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-21690-4_14"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491456"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.2197\/ipsjjip.27.810"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498707","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3498707","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T19:30:28Z","timestamp":1750188628000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3498707"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,1,12]]},"references-count":60,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2022,1,16]]}},"alternative-id":["10.1145\/3498707"],"URL":"https:\/\/doi.org\/10.1145\/3498707","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,1,12]]},"assertion":[{"value":"2022-01-12","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}