{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,30]],"date-time":"2026-01-30T00:24:11Z","timestamp":1769732651501,"version":"3.49.0"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100010663","name":"H2020 European Research Council","doi-asserted-by":"publisher","award":["759969"],"award-info":[{"award-number":["759969"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61472474,61572478"],"award-info":[{"award-number":["61472474,61572478"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"INRIA-CAS","award":["Verification, Interaction, and Proofs"],"award-info":[{"award-number":["Verification, Interaction, and Proofs"]}]},{"DOI":"10.13039\/501100000923","name":"Australian Research Council","doi-asserted-by":"publisher","award":["DP160101652"],"award-info":[{"award-number":["DP160101652"]}],"id":[{"id":"10.13039\/501100000923","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/P00430X\/1,EP\/K009907\/1"],"award-info":[{"award-number":["EP\/P00430X\/1,EP\/K009907\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2018,1]]},"abstract":"<jats:p>The theory of strings with concatenation has been widely argued as the basis of constraint solving for verifying string-manipulating programs. However, this theory is far from adequate for expressing many string constraints that are also needed in practice; for example, the use of regular constraints (pattern matching against a regular expression), and the string-replace function (replacing either the first occurrence or all occurrences of a ``pattern'' string constant\/variable\/regular expression by a ``replacement'' string constant\/variable), among many others. Both regular constraints and the string-replace function are crucial for such applications as analysis of JavaScript (or more generally HTML5 applications) against cross-site scripting (XSS) vulnerabilities, which motivates us to consider a richer class of string constraints. The importance of the string-replace function (especially the replace-all facility) is increasingly recognised, which can be witnessed by the incorporation of the function in the input languages of several string constraint solvers.<\/jats:p>\n          <jats:p>Recently, it was shown that any theory of strings containing the string-replace function (even the most restricted version where pattern\/replacement strings are both constant strings) becomes undecidable if we do not impose some kind of straight-line (aka acyclicity) restriction on the formulas. Despite this, the straight-line restriction is still practically sensible since this condition is typically met by string constraints that are generated by symbolic execution. In this paper, we provide the first systematic study of straight-line string constraints with the string-replace function and the regular constraints as the basic operations. We show that a large class of such constraints (i.e. when only a constant string or a regular expression is permitted in the pattern) is decidable. We note that the string-replace function, even under this restriction, is sufficiently powerful for expressing the concatenation operator and much more (e.g. extensions of regular expressions with string variables). This gives us the most expressive decidable logic containing concatenation, replace, and regular constraints under the same umbrella. Our decision procedure for the straight-line fragment follows an automata-theoretic approach, and is modular in the sense that the string-replace terms are removed one by one to generate more and more regular constraints, which can then be discharged by the state-of-the-art string constraint solvers. We also show that this fragment is, in a way, a maximal decidable subclass of the straight-line fragment with string-replace and regular constraints. To this end, we show undecidability results for the following two extensions: (1) variables are permitted in the pattern parameter of the replace function, (2) length constraints are permitted.<\/jats:p>","DOI":"10.1145\/3158091","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":36,"title":["What is decidable about string constraints with the ReplaceAll function"],"prefix":"10.1145","volume":"2","author":[{"given":"Taolue","family":"Chen","sequence":"first","affiliation":[{"name":"University of London, UK"}]},{"given":"Yan","family":"Chen","sequence":"additional","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, China \/ University at Chinese Academy of Sciences, China"}]},{"given":"Matthew","family":"Hague","sequence":"additional","affiliation":[{"name":"Royal Holloway University of London, UK"}]},{"given":"Anthony W.","family":"Lin","sequence":"additional","affiliation":[{"name":"University of Oxford, UK"}]},{"given":"Zhilin","family":"Wu","sequence":"additional","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, China"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"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.1007\/978-3-319-08867-9_10"},{"key":"e_1_2_2_3_1","volume-title":"IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010","author":"Alur Rajeev","year":"2010","unstructured":"Rajeev Alur and Pavol Cern\u00fd . 2010 . Expressiveness of streaming string transducers . In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010 , December 15-18, 2010, Chennai, India. 1\u201312. Rajeev Alur and Pavol Cern\u00fd. 2010. Expressiveness of streaming string transducers. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, December 15-18, 2010, Chennai, India. 1\u201312."},{"key":"e_1_2_2_4_1","volume-title":"Principles of Model Checking (Representation and Mind Series)","author":"Baier Christel","unstructured":"Christel Baier and Joost-Pieter Katoen . 2008. Principles of Model Checking (Representation and Mind Series) . The MIT Press . Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking (Representation and Mind Series). The MIT Press."},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2008.22"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_27"},{"key":"e_1_2_2_7_1","volume-title":"The Collected Works of J. Richard B\u00fcchi","author":"Richard B\u00fcchi J","unstructured":"J Richard B\u00fcchi and Steven Senger . 1990. Definability in the existential theory of concatenation and undecidable extensions of this theory . In The Collected Works of J. Richard B\u00fcchi . Springer , 671\u2013683. J Richard B\u00fcchi and Steven Senger. 1990. Definability in the existential theory of concatenation and undecidable extensions of this theory. In The Collected Works of J. Richard B\u00fcchi. Springer, 671\u2013683."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1180405.1180445"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_13"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_14"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39611-3_21"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1064978.1065036"},{"key":"e_1_2_2_13_1","volume-title":"https:\/\/developers.google.com\/closure\/templates\/ . Referred","author":"Templates Closure","year":"2017","unstructured":"Google. 2015. Closure Templates . https:\/\/developers.google.com\/closure\/templates\/ . Referred July 2017 . Google. 2015. Closure Templates. https:\/\/developers.google.com\/closure\/templates\/ . Referred July 2017."},{"key":"e_1_2_2_14_1","volume-title":"Fast and Precise Sanitizer Analysis with BEK. In USENIX Security Symposium.","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. Pieter Hooimeijer, Benjamin Livshits, David Molnar, Prateek Saxena, and Margus Veanes. 2011. Fast and Precise Sanitizer Analysis with BEK. In USENIX Security Symposium."},{"key":"e_1_2_2_15_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_16_1","volume-title":"Word equations in linear space. CoRR abs\/1702.00736","author":"Jez Artur","year":"2017","unstructured":"Artur Jez . 2017. Word equations in linear space. CoRR abs\/1702.00736 ( 2017 ). http:\/\/arxiv.org\/abs\/1702.00736 Artur Jez. 2017. Word equations in linear space. CoRR abs\/1702.00736 (2017). http:\/\/arxiv.org\/abs\/1702.00736"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2643134"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2377656.2377662"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_2_20_1","volume-title":"mustache.js. https:\/\/github.com\/janl\/mustache.js\/ . Referred","author":"Lehnardt Jan","year":"2017","unstructured":"Jan Lehnardt and contributors. 2015. mustache.js. https:\/\/github.com\/janl\/mustache.js\/ . Referred July 2017 . Jan Lehnardt and contributors. 2015. mustache.js. https:\/\/github.com\/janl\/mustache.js\/ . Referred July 2017."},{"key":"e_1_2_2_21_1","doi-asserted-by":"crossref","unstructured":"Tianyi Liang Andrew Reynolds Cesare Tinelli Clark Barrett and Morgan Deters. 2014. A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions. In CAV. 646\u2013662.  Tianyi Liang Andrew Reynolds Cesare Tinelli Clark Barrett and Morgan Deters. 2014. A DPLL(T) Theory Solver for a Theory of Strings and Regular Expressions. In CAV. 646\u2013662.","DOI":"10.1007\/978-3-319-08867-9_43"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837641"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1070\/SM1977v032n02ABEH002376"},{"key":"e_1_2_2_24_1","volume-title":"Hilbert\u2019s Tenth Problem","author":"Matiyasevich Yuri V.","unstructured":"Yuri V. Matiyasevich . 1993. Hilbert\u2019s Tenth Problem . MIT Press , Cambridge, MA, USA . Yuri V. Matiyasevich. 1993. Hilbert\u2019s Tenth Problem. MIT Press, Cambridge, MA, USA."},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/990308.990312"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.38"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55124-7_4"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491447"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660372"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_12"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103674"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4"},{"key":"e_1_2_2_34_1","volume-title":"Mustache: Logic-less Templates. https:\/\/mustache.github.io\/ . Referred","author":"Wanstrath Chris","year":"2009","unstructured":"Chris Wanstrath . 2009 . Mustache: Logic-less Templates. https:\/\/mustache.github.io\/ . Referred July 2017. Chris Wanstrath. 2009. Mustache: Logic-less Templates. https:\/\/mustache.github.io\/ . Referred July 2017."},{"key":"e_1_2_2_35_1","volume-title":"XSS Prevention Cheat Sheet. https:\/\/www.owasp.org\/index.php\/XSS_ (Cross_Site_Scripting)_Prevention_Cheat_Sheet . Referred","author":"Williams Jeff","year":"2017","unstructured":"Jeff Williams , Jim Manico , and Neil Mattatall . 2017. XSS Prevention Cheat Sheet. https:\/\/www.owasp.org\/index.php\/XSS_ (Cross_Site_Scripting)_Prevention_Cheat_Sheet . Referred July 2017 . Jeff Williams, Jim Manico, and Neil Mattatall. 2017. XSS Prevention Cheat Sheet. https:\/\/www.owasp.org\/index.php\/XSS_ (Cross_Site_Scripting)_Prevention_Cheat_Sheet . Referred July 2017."},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-013-0189-1"},{"key":"e_1_2_2_37_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\/10.1145\/3158091","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158091","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158091"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":37,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158091"],"URL":"https:\/\/doi.org\/10.1145\/3158091","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}