{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T10:37:08Z","timestamp":1790937428082,"version":"4.1.0"},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K009907\/1,EP\/P00430X\/1"],"award-info":[{"award-number":["EP\/K009907\/1,EP\/P00430X\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"crossref","award":["61472474,61572478,61872340"],"award-info":[{"award-number":["61472474,61572478,61872340"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100013102","name":"Australian Research Council","doi-asserted-by":"publisher","award":["DP160101652, DP180100691"],"award-info":[{"award-number":["DP160101652, DP180100691"]}],"id":[{"id":"10.13039\/100013102","id-type":"DOI","asserted-by":"publisher"}]},{"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\/501100004359","name":"Vetenskapsr\u00e5det","doi-asserted-by":"publisher","award":["2014-5484"],"award-info":[{"award-number":["2014-5484"]}],"id":[{"id":"10.13039\/501100004359","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100011751","name":"Stiftelsen f\u00f6r Strategisk Forskning","doi-asserted-by":"crossref","award":["RIT17-0011"],"award-info":[{"award-number":["RIT17-0011"]}],"id":[{"id":"10.13039\/501100011751","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":[[2019,1,2]]},"abstract":"<jats:p>The design and implementation of decision procedures for checking path feasibility in string-manipulating programs is an important problem, with such applications as symbolic execution of programs with strings and automated detection of cross-site scripting (XSS) vulnerabilities in web applications. A (symbolic) path is given as a finite sequence of assignments and assertions (i.e. without loops), and checking its feasibility amounts to determining the existence of inputs that yield a successful execution. Modern programming languages (e.g. JavaScript, PHP, and Python) support many complex string operations, and strings are also often implicitly modified during a computation in some intricate fashion (e.g. by some autoescaping mechanisms).<\/jats:p>\n          <jats:p>\n            In this paper we provide two general semantic conditions which together ensure the decidability of path feasibility: (1) each assertion admits regular monadic decomposition (i.e. is an effectively recognisable relation), and (2) each assignment uses a (possibly nondeterministic) function whose inverse relation preserves regularity. We show that the semantic conditions are\n            <jats:italic>expressive<\/jats:italic>\n            since they are satisfied by a multitude of string operations including concatenation, one-way and two-way finite-state transducers, replaceall functions (where the replacement string could contain variables), string-reverse functions, regular-expression matching, and some (restricted) forms of letter-counting\/length functions. The semantic conditions also strictly subsume existing decidable string theories (e.g. straight-line fragments, and acyclic logics), and most existing benchmarks (e.g. most of Kaluza\u2019s, and all of SLOG\u2019s, Stranger\u2019s, and SLOTH\u2019s benchmarks). Our semantic conditions also yield a conceptually\n            <jats:italic>simple<\/jats:italic>\n            decision procedure, as well as an\n            <jats:italic>extensible<\/jats:italic>\n            architecture of a string solver in that a user may easily incorporate his\/her own string functions into the solver by simply providing code for the pre-image computation without worrying about other parts of the solver. Despite these, the semantic conditions are unfortunately too general to provide a fast and complete decision procedure. We provide strong theoretical evidence for this in the form of complexity results. To rectify this problem, we propose two solutions. Our main solution is to allow only partial string functions (i.e., prohibit nondeterminism) in condition (2). This restriction is satisfied in many cases in practice, and yields decision procedures that are effective in both theory and practice. Whenever nondeterministic functions are still needed (e.g. the string function split), our second solution is to provide a syntactic fragment that provides a support of nondeterministic functions, and operations like one-way transducers, replaceall (with constant replacement string), the string-reverse function, concatenation, and regular-expression matching. We show that this fragment can be reduced to an existing solver SLOTH that exploits fast model checking algorithms like IC3.\n          <\/jats:p>\n          <jats:p>We provide an efficient implementation of our decision procedure (assuming our first solution above, i.e., deterministic partial string functions) in a new string solver OSTRICH. Our implementation provides built-in support for concatenation, reverse, functional transducers (FFT), and replaceall and provides a framework for extensibility to support further string functions. We demonstrate the efficacy of our new solver against other competitive solvers.<\/jats:p>","DOI":"10.1145\/3290362","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":67,"title":["Decision procedures for path feasibility of string-manipulating programs with complex operations"],"prefix":"10.1145","volume":"3","author":[{"given":"Taolue","family":"Chen","sequence":"first","affiliation":[{"name":"Birkbeck University of London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthew","family":"Hague","sequence":"additional","affiliation":[{"name":"Royal Holloway University of London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Anthony W.","family":"Lin","sequence":"additional","affiliation":[{"name":"University of Oxford, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Philipp","family":"R\u00fcmmer","sequence":"additional","affiliation":[{"name":"Uppsala University, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Zhilin","family":"Wu","sequence":"additional","affiliation":[{"name":"Institute of Software at Chinese Academy of Sciences, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062384"},{"key":"e_1_2_2_2_1","volume-title":"FMCAD","author":"Abdulla Parosh Aziz","year":"2018","unstructured":"Parosh Aziz Abdulla , Mohamed Faouzi Atig , Yu-Fang Chen , Bui Phi Diep , Luk\u00e1s Hol\u00edk , Ahmed Rezine , and Philipp R\u00fcmmer . 2018 . TRAU: SMT Solver for String Constraints. In Formal Methods in Computer Aided Design , FMCAD 2018. To appear. Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Luk\u00e1s Hol\u00edk, Ahmed Rezine, and Philipp R\u00fcmmer. 2018. TRAU: SMT Solver for String Constraints. In Formal Methods in Computer Aided Design, FMCAD 2018. To appear."},{"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","volume-title":"38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2011, Proceedings, Part II. Springer, 1\u201320","author":"Alur Rajeev","unstructured":"Rajeev Alur and Jyotirmoy V. Deshmukh . 2011. Nondeterministic Streaming String Transducers. In Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2011, Proceedings, Part II. Springer, 1\u201320 . Rajeev Alur and Jyotirmoy V. Deshmukh. 2011. Nondeterministic Streaming String Transducers. In Automata, Languages and Programming - 38th International Colloquium, ICALP 2011, Zurich, Switzerland, July 4-8, 2011, Proceedings, Part II. Springer, 1\u201320."},{"key":"e_1_2_2_5_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_6_1","volume-title":"Graph Logics with Rational Relations. Logical Methods in Computer Science 9, 3","author":"Barcel\u00f3 Pablo","year":"2013","unstructured":"Pablo Barcel\u00f3 , Diego Figueira , and Leonid Libkin . 2013. Graph Logics with Rational Relations. Logical Methods in Computer Science 9, 3 ( 2013 ). Pablo Barcel\u00f3, Diego Figueira, and Leonid Libkin. 2013. Graph Logics with Rational Relations. Logical Methods in Computer Science 9, 3 (2013)."},{"key":"e_1_2_2_7_1","volume-title":"Handbook of Satisfiability","author":"Barrett Clark W.","unstructured":"Clark W. Barrett , Roberto Sebastiani , Sanjit A. Seshia , and Cesare Tinelli . 2009. Satisfiability Modulo Theories . In Handbook of Satisfiability . IOS Press , 825\u2013885. Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. 2009. Satisfiability Modulo Theories. In Handbook of Satisfiability. IOS Press, 825\u2013885."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876642"},{"key":"e_1_2_2_9_1","volume-title":"FMCAD 2017","author":"Berzish Murphy","year":"2017","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 2017 , Vienna, Austria , October 2-6, 2017. IEEE, 55\u201359. 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 2017, Vienna, Austria, October 2-6, 2017. IEEE, 55\u201359."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_27"},{"key":"e_1_2_2_11_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_12_1","volume-title":"The Complexity of Games on Higher Order Pushdown Automata. CoRR abs\/0705.0262","author":"Cachat Thierry","year":"2007","unstructured":"Thierry Cachat and Igor Walukiewicz . 2007. The Complexity of Games on Higher Order Pushdown Automata. CoRR abs\/0705.0262 ( 2007 ). arXiv: 0705.0262 http:\/\/arxiv.org\/abs\/0705.0262 Thierry Cachat and Igor Walukiewicz. 2007. The Complexity of Games on Higher Order Pushdown Automata. CoRR abs\/0705.0262 (2007). arXiv: 0705.0262 http:\/\/arxiv.org\/abs\/0705.0262"},{"key":"e_1_2_2_13_1","volume-title":"Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908)","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , and Dawson Engler . 2008 . KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs . In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908) . USENIX Association, Berkeley, CA, USA, 209\u2013224. http:\/\/dl.acm.org\/citation.cfm?id= 1855741. 1855756 Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI\u201908). USENIX Association, Berkeley, CA, USA, 209\u2013224. http:\/\/dl.acm.org\/citation.cfm?id=1855741. 1855756"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1180405.1180445"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"key":"e_1_2_2_16_1","first-page":"255","article-title":"Decision problems among the main subfamilies of rational relations","volume":"40","author":"Carton Olivier","year":"2006","unstructured":"Olivier Carton , Christian Choffrut , and Serge Grigorieff . 2006 . Decision problems among the main subfamilies of rational relations . ITA 40 , 2 (2006), 255 \u2013 275 . Olivier Carton, Christian Choffrut, and Serge Grigorieff. 2006. Decision problems among the main subfamilies of rational relations. ITA 40, 2 (2006), 255\u2013275.","journal-title":"ITA"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158091"},{"key":"e_1_2_2_18_1","volume-title":"Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations. CoRR abs\/1811.03167","author":"Chen Taolue","year":"2018","unstructured":"Taolue Chen , Matthew Hague , Anthony W. Lin , Philipp R\u00fcmmer , and Zhilin Wu. 2018b. Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations. CoRR abs\/1811.03167 ( 2018 ). arXiv: 1811.03167 https:\/\/arxiv.org\/abs\/1811.03167 Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp R\u00fcmmer, and Zhilin Wu. 2018b. Decision Procedures for Path Feasibility of String-Manipulating Programs with Complex Operations. CoRR abs\/1811.03167 (2018). arXiv: 1811.03167 https:\/\/arxiv.org\/abs\/1811.03167"},{"key":"e_1_2_2_19_1","volume-title":"Solving String Constraints with ReplaceAll Function. Master\u2019s thesis. State Key Laboratory of Computer Science","author":"Chen Yan","unstructured":"Yan Chen . 2018a. Solving String Constraints with ReplaceAll Function. Master\u2019s thesis. State Key Laboratory of Computer Science , Institute of Software , Chinese Academy of Sciences, China. Yan Chen. 2018a. Solving String Constraints with ReplaceAll Function. Master\u2019s thesis. State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, China."},{"key":"e_1_2_2_20_1","volume-title":"https:\/\/github.com\/TinyYan\/z3- replaceAll . Referred","author":"Chen Yan","year":"2018","unstructured":"Yan Chen . 2018b. Z3-replaceall. https:\/\/github.com\/TinyYan\/z3- replaceAll . Referred in Jan 2018 . Yan Chen. 2018b. Z3-replaceall. https:\/\/github.com\/TinyYan\/z3- replaceAll . Referred in Jan 2018."},{"key":"e_1_2_2_21_1","first-page":"159","article-title":"Relations over Words and Logic: A Chronology","volume":"89","author":"Choffrut Christian","year":"2006","unstructured":"Christian Choffrut . 2006 . Relations over Words and Logic: A Chronology . Bulletin of the EATCS 89 (2006), 159 \u2013 163 . Christian Choffrut. 2006. Relations over Words and Logic: A Chronology. Bulletin of the EATCS 89 (2006), 159\u2013163.","journal-title":"Bulletin of the EATCS"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_14"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1995376.1995394"},{"key":"e_1_2_2_24_1","volume-title":"Theory of Graphs. Gordon &amp","author":"D\u00e9nes J.","unstructured":"J. D\u00e9nes . 1967. Connections between transformation semigroups and graphs . In Theory of Graphs. Gordon &amp ; Breach . J. D\u00e9nes. 1967. Connections between transformation semigroups and graphs. In Theory of Graphs. Gordon &amp; Breach."},{"key":"e_1_2_2_25_1","volume-title":"Algebraic Combinatorics on Words","author":"Diekert Volker","unstructured":"Volker Diekert . 2002. Makanin\u2019s Algorithm . In Algebraic Combinatorics on Words , M. Lothaire (Ed.). Encyclopedia of Mathematics and its Applications, Vol. 90 . Cambridge University Press , Chapter 12, 387\u2013442. Volker Diekert. 2002. Makanin\u2019s Algorithm. In Algebraic Combinatorics on Words, M. Lothaire (Ed.). Encyclopedia of Mathematics and its Applications, Vol. 90. Cambridge University Press, Chapter 12, 387\u2013442."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/371316.371512"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/2591370.2591389"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39611-3_21"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1064978.1065036"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158092"},{"key":"e_1_2_2_31_1","volume-title":"Fast and Precise Sanitizer Analysis with BEK. In 20th 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 20th USENIX Security Symposium , San Francisco, CA, USA , August 8-12, 2011, Proceedings. USENIX Association. 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 20th USENIX Security Symposium, San Francisco, CA, USA, August 8-12, 2011, Proceedings. USENIX Association. http:\/\/static.usenix.org\/events\/sec11\/tech\/full_papers\/Hooimeijer.pdf"},{"key":"e_1_2_2_32_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_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2743014"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800003889"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2643134"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2377656.2377662"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_2_38_1","volume-title":"Automata and Computability","author":"Kozen Dexter","unstructured":"Dexter Kozen . 1997. Automata and Computability . Springer . Dexter Kozen. 1997. Automata and Computability. Springer."},{"key":"e_1_2_2_39_1","volume-title":"Decision Procedures","author":"Kroening Daniel","unstructured":"Daniel Kroening and Ofer Strichman . 2008. Decision Procedures . Springer . Daniel Kroening and Ofer Strichman. 2008. Decision Procedures. Springer."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_43"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/937555.937557"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837641"},{"key":"e_1_2_2_43_1","volume-title":"Symbolic model checking","author":"McMillan K. L.","unstructured":"K. L. McMillan . 1993. Symbolic model checking . Kluwer . K. L. McMillan. 1993. Symbolic model checking. Kluwer."},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1060745.1060809"},{"key":"e_1_2_2_45_1","volume-title":"Third International Conference, FOSSACS","author":"Morvan Christophe","year":"2000","unstructured":"Christophe Morvan . 2000 . On Rational Graphs. In Foundations of Software Science and Computation Structures , Third International Conference, FOSSACS 2000. Springer, 252\u2013266. Christophe Morvan. 2000. On Rational Graphs. In Foundations of Software Science and Computation Structures, Third International Conference, FOSSACS 2000. Springer, 252\u2013266."},{"key":"e_1_2_2_46_1","volume-title":"11th International Conference, LPAR 2004 (LNCS)","volume":"3452","author":"Nieuwenhuis Robert","year":"2004","unstructured":"Robert Nieuwenhuis , Albert Oliveras , and Cesare Tinelli . 2004 . Abstract DPLL and Abstract DPLL Modulo Theories. In Logic for Programming, Artificial Intelligence, and Reasoning , 11th International Conference, LPAR 2004 (LNCS) , Vol. 3452 . Springer, 36\u201350. Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli. 2004. Abstract DPLL and Abstract DPLL Modulo Theories. In Logic for Programming, Artificial Intelligence, and Reasoning, 11th International Conference, LPAR 2004 (LNCS), Vol. 3452. Springer, 36\u201350."},{"key":"e_1_2_2_47_1","volume-title":"Theories of Computability","author":"Pippenger Nicholas","unstructured":"Nicholas Pippenger . 2010. Theories of Computability . Cambridge University Press . Nicholas Pippenger. 2010. Theories of Computability. Cambridge University Press."},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/990308.990312"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89439-1_20"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.38"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491447"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081750"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660372"},{"key":"e_1_2_2_54_1","volume-title":"CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I. Springer, 218\u2013240","author":"Trinh Minh-Thai","year":"2016","unstructured":"Minh-Thai Trinh , Duc-Hiep Chu , and Joxan Jaffar . 2016 . Progressive Reasoning over Recursively-Defined Strings. In Computer Aided Verification - 28th International Conference , CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I. Springer, 218\u2013240 . Minh-Thai Trinh, Duc-Hiep Chu, and Joxan Jaffar. 2016. Progressive Reasoning over Recursively-Defined Strings. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I. Springer, 218\u2013240."},{"key":"e_1_2_2_55_1","volume-title":"https:\/\/www.owasp. org\/index.php\/Top_10- 2017_Top_10 . Referred","author":"van der Stock Andrew","year":"2018","unstructured":"Andrew van der Stock , Brian Glas , Neil Smithline , and Torsten Gigler . 2017. OWASP Top 10 \u2013 2017. https:\/\/www.owasp. org\/index.php\/Top_10- 2017_Top_10 . Referred January 2018 . Andrew van der Stock, Brian Glas, Neil Smithline, and Torsten Gigler. 2017. OWASP Top 10 \u2013 2017. https:\/\/www.owasp. org\/index.php\/Top_10- 2017_Top_10 . Referred January 2018."},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3040488"},{"key":"e_1_2_2_57_1","volume-title":"CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I (Lecture Notes in Computer Science)","volume":"9779","author":"Wang Hung-En","unstructured":"Hung-En Wang , Tzung-Lin Tsai , Chun-Han Lin , Fang Yu , and Jie-Hong R. Jiang . 2016. String Analysis via Automata Manipulation with Logic Circuit Representation. In Computer Aided Verification - 28th International Conference , CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I (Lecture Notes in Computer Science) , Vol. 9779 . Springer, 241\u2013260. Hung-En Wang, Tzung-Lin Tsai, Chun-Han Lin, Fang Yu, and Jie-Hong R. Jiang. 2016. String Analysis via Automata Manipulation with Logic Circuit Representation. In Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part I (Lecture Notes in Computer Science), Vol. 9779. Springer, 241\u2013260."},{"key":"e_1_2_2_58_1","volume-title":"Eui Chul Richard Shin, and Dawn Song","author":"Weinberger Joel","year":"2011","unstructured":"Joel Weinberger , Prateek Saxena , Devdatta Akhawe , Matthew Finifter , Eui Chul Richard Shin, and Dawn Song . 2011 . A Systematic Analysis of XSS Sanitization in Web Application Frameworks. In Computer Security - ESORICS 2011 - 16th European Symposium on Research in Computer Security, Leuven, Belgium, September 12-14, 2011. Proceedings. Springer , 150\u2013171. Joel Weinberger, Prateek Saxena, Devdatta Akhawe, Matthew Finifter, Eui Chul Richard Shin, and Dawn Song. 2011. A Systematic Analysis of XSS Sanitization in Web Application Frameworks. In Computer Security - ESORICS 2011 - 16th European Symposium on Research in Computer Security, Leuven, Belgium, September 12-14, 2011. Proceedings. Springer, 150\u2013171."},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_13"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-013-0189-1"},{"key":"e_1_2_2_61_1","volume-title":"Graphs of semigroups. \u010casopis pro p\u011bstov\u00e1n\u00ed matematiky 106, 4","author":"Zelinka Bohdan","year":"1981","unstructured":"Bohdan Zelinka . 1981. Graphs of semigroups. \u010casopis pro p\u011bstov\u00e1n\u00ed matematiky 106, 4 ( 1981 ), 407\u2013408. http:\/\/eudml.org\/ doc\/19323 Bohdan Zelinka. 1981. Graphs of semigroups. \u010casopis pro p\u011bstov\u00e1n\u00ed matematiky 106, 4 (1981), 407\u2013408. http:\/\/eudml.org\/ doc\/19323"},{"key":"e_1_2_2_62_1","volume-title":"CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. Springer, 235\u2013254","author":"Zheng Yunhui","year":"2015","unstructured":"Yunhui Zheng , Vijay Ganesh , Sanu Subramanian , Omer Tripp , Julian Dolby , and Xiangyu Zhang . 2015 . Effective Search-Space Pruning for Solvers of String Equations, Regular Expressions and Length Constraints. In Computer Aided Verification -27th International Conference , CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. Springer, 235\u2013254 . Yunhui Zheng, Vijay Ganesh, Sanu Subramanian, Omer Tripp, Julian Dolby, and Xiangyu Zhang. 2015. Effective Search-Space Pruning for Solvers of String Equations, Regular Expressions and Length Constraints. In Computer Aided Verification -27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I. Springer, 235\u2013254."},{"key":"e_1_2_2_63_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\/3290362","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290362","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290362"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":63,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290362"],"URL":"https:\/\/doi.org\/10.1145\/3290362","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}