{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:49Z","timestamp":1772164009300,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":74,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,1,11]],"date-time":"2016-01-11T00:00:00Z","timestamp":1452470400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,1,11]]},"DOI":"10.1145\/2837614.2837641","type":"proceedings-article","created":{"date-parts":[[2016,1,7]],"date-time":"2016-01-07T09:05:00Z","timestamp":1452157500000},"page":"123-136","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":42,"title":["String solving with word equations and transducers: towards a logic for analysing mutation XSS"],"prefix":"10.1145","author":[{"given":"Anthony W.","family":"Lin","sequence":"first","affiliation":[{"name":"Yale-NUS College, Singapore"}]},{"given":"Pablo","family":"Barcel\u00f3","sequence":"additional","affiliation":[{"name":"University of Chile, Chile"}]}],"member":"320","published-online":{"date-parts":[[2016,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"BEK website (referred in Nov 2015). http:\/\/research. microsoft.com\/en-us\/projects\/bek\/.  BEK website (referred in Nov 2015). http:\/\/research. microsoft.com\/en-us\/projects\/bek\/."},{"key":"e_1_3_2_1_2_1","unstructured":"OWASP XSS cheat sheet (referred in Nov 2015). https: \/\/www.owasp.org\/index.php\/XSS_(Cross_Site_Scripting) _Prevention_Cheat_Sheet.  OWASP XSS cheat sheet (referred in Nov 2015). https: \/\/www.owasp.org\/index.php\/XSS_(Cross_Site_Scripting) _Prevention_Cheat_Sheet."},{"key":"e_1_3_2_1_3_1","unstructured":"SAT competition (referred in Nov 2015). http:\/\/www. satcompetition.org\/.  SAT competition (referred in Nov 2015). http:\/\/www. satcompetition.org\/."},{"key":"e_1_3_2_1_4_1","unstructured":"SMT competition (referred in Nov 2015). http:\/\/www.smtcomp. org\/.  SMT competition (referred in Nov 2015). http:\/\/www.smtcomp. org\/."},{"key":"e_1_3_2_1_5_1","unstructured":"Google Closure Library (referred in Nov 2015). https:\/\/ developers.google.com\/closure\/library\/.  Google Closure Library (referred in Nov 2015). https:\/\/ developers.google.com\/closure\/library\/."},{"key":"e_1_3_2_1_6_1","unstructured":"HTML5 Security cheat sheet (referred in Nov 2015). http:\/\/ html5sec.org\/.  HTML5 Security cheat sheet (referred in Nov 2015). http:\/\/ html5sec.org\/."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_10"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2008.22"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2389241.2389250"},{"key":"e_1_3_2_1_10_1","volume-title":"Graph logics with rational relations. Logical Methods in Computer Science, 9(3)","author":"Barcel\u00f3 P.","year":"2013","unstructured":"P. Barcel\u00f3 , D. Figueira , and L. Libkin . Graph logics with rational relations. Logical Methods in Computer Science, 9(3) , 2013 .. P. Barcel\u00f3, D. Figueira, and L. Libkin. Graph logics with rational relations. Logical Methods in Computer Science, 9(3), 2013.."},{"key":"e_1_3_2_1_11_1","first-page":"885","volume-title":"Biere et al. {15}","author":"Barrett C. W.","unstructured":"C. W. Barrett , R. Sebastiani , S. A. Seshia , and C. Tinelli . Satisfiability modulo theories . In Biere et al. {15} , pages 825\u2013 885 .. C. W. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli. Satisfiability modulo theories. In Biere et al. {15}, pages 825\u2013885.."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03092-5_2"},{"key":"e_1_3_2_1_13_1","volume-title":"Symbolic model checking of tense logics on rational Kripke models. CoRR, abs\/0810.5516","author":"Bekker W.","year":"2008","unstructured":"W. Bekker and V. Goranko . Symbolic model checking of tense logics on rational Kripke models. CoRR, abs\/0810.5516 , 2008 . W. Bekker and V. Goranko. Symbolic model checking of tense logics on rational Kripke models. CoRR, abs\/0810.5516, 2008."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-663-09367-1"},{"key":"e_1_3_2_1_15_1","series-title":"Frontiers in Artificial Intelligence and Applications","volume-title":"Handbook of Satisfiability","author":"Biere A.","year":"2009","unstructured":"A. Biere , M. Heule , H. van Maaren , and T. Walsh , editors . Handbook of Satisfiability , volume 185 of Frontiers in Artificial Intelligence and Applications , 2009 . IOS Press . A. Biere, M. Heule, H. van Maaren, and T. Walsh, editors. Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, 2009. IOS Press."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_27"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/788022.789015"},{"issue":"6","key":"e_1_3_2_1_18_1","first-page":"641","volume":"37","author":"Blumensath A.","year":"2004","unstructured":"A. Blumensath and E. Gr\u00e4del . Finite Presentations of Infinite Structures: Automata and Interpretations. Theory Comput. Syst. , 37 ( 6 ): 641 \u2013 674 , 2004 . A. Blumensath and E. Gr\u00e4del. Finite Presentations of Infinite Structures: Automata and Interpretations. Theory Comput. Syst., 37(6):641\u2013 674, 2004.","journal-title":"Finite Presentations of Infinite Structures: Automata and Interpretations. Theory Comput. Syst."},{"key":"e_1_3_2_1_19_1","first-page":"683","volume-title":"The Collected Works of J. Richard B\u00fcchi","author":"B\u00fcchi J. R.","unstructured":"J. R. B\u00fcchi and S. Senger . Definability in the existential theory of concatenation and undecidable extensions of this theory . In The Collected Works of J. Richard B\u00fcchi , pages 671\u2013 683 . Springer, 1990. J. R. B\u00fcchi and S. Senger. Definability in the existential theory of concatenation and undecidable extensions of this theory. In The Collected Works of J. Richard B\u00fcchi, pages 671\u2013683. Springer, 1990."},{"issue":"2","key":"e_1_3_2_1_20_1","first-page":"255","article-title":"Decision problems among the main subfamilies of rational relations","volume":"40","author":"Carton O.","year":"2006","unstructured":"O. Carton , C. Choffrut , and S. Grigorieff . Decision problems among the main subfamilies of rational relations . ITA , 40 ( 2 ): 255 \u2013 275 , 2006 . O. Carton, C. Choffrut, and S. Grigorieff. Decision problems among the main subfamilies of rational relations. ITA, 40(2):255\u2013275, 2006.","journal-title":"ITA"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/1760267.1760269"},{"key":"e_1_3_2_1_22_1","volume-title":"Introduction to Algorithms","author":"Cormen T. H.","year":"2009","unstructured":"T. H. Cormen , C. E. Leiserson , R. L. Rivest , and C. Stein . Introduction to Algorithms , Third Edition. The MIT Press , 3 rd edition, 2009 . ISBN 0262033844, 9780262033848. T. H. Cormen, C. E. Leiserson, R. L. Rivest, and C. Stein. Introduction to Algorithms, Third Edition. The MIT Press, 3rd edition, 2009. ISBN 0262033844, 9780262033848."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35873-9_14"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1995376.1995394"},{"key":"e_1_3_2_1_25_1","series-title":"Encyclopedia of Mathematics and its Applications","first-page":"442","volume-title":"Algebraic Combinatorics on Words","author":"Diekert V.","unstructured":"V. Diekert . Makanin\u2019s Algorithm . In M. Lothaire, editor, Algebraic Combinatorics on Words , volume 90 of Encyclopedia of Mathematics and its Applications , chapter 12, pages 387\u2013 442 . Cambridge University Press, 2002. V. Diekert. Makanin\u2019s Algorithm. In M. Lothaire, editor, Algebraic Combinatorics on Words, volume 90 of Encyclopedia of Mathematics and its Applications, chapter 12, pages 387\u2013442. Cambridge University Press, 2002."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2008.923410"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2011.03.019"},{"key":"e_1_3_2_1_28_1","first-page":"76","volume-title":"NFM","author":"Fu X.","year":"2010","unstructured":"X. Fu and C. Li . Modeling regular replacement for string constraint solving . In NFM , pages 67\u2013 76 , 2010 . X. Fu and C. Li. Modeling regular replacement for string constraint solving. In NFM, pages 67\u201376, 2010."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-011-0214-3"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39611-3_21"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/998675.999468"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2508859.2516723"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/1946284.1946302"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-012-0111-x"},{"key":"e_1_3_2_1_35_1","volume-title":"USENIX Security Symposium","author":"Hooimeijer P.","year":"2011","unstructured":"P. Hooimeijer , B. Livshits , D. Molnar , P. Saxena , and M. Veanes . Fast and precise sanitizer analysis with BEK . In USENIX Security Symposium , 2011 . URL http:\/\/static.usenix.org\/events\/ sec11\/tech\/full_papers\/Hooimeijer.pdf. P. Hooimeijer, B. Livshits, D. Molnar, P. Saxena, and M. Veanes. Fast and precise sanitizer analysis with BEK. In USENIX Security Symposium, 2011. URL http:\/\/static.usenix.org\/events\/ sec11\/tech\/full_papers\/Hooimeijer.pdf."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/322047.322058"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/2643134"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2377656.2377662"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1142\/S012905410200128X"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2010.21"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.16"},{"key":"e_1_3_2_1_42_1","volume-title":"Decision Procedures","author":"Kroening D.","year":"2008","unstructured":"D. Kroening and O. Strichman . Decision Procedures . Springer , 2008 . D. Kroening and O. Strichman. Decision Procedures. Springer, 2008."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_43"},{"key":"e_1_3_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837641"},{"issue":"2","key":"e_1_3_2_1_45_1","first-page":"129","article-title":"The problem of solvability of equations in a free semigroup. Sbornik","volume":"32","author":"Makanin G. S.","year":"1977","unstructured":"G. S. Makanin . The problem of solvability of equations in a free semigroup. Sbornik : Mathematics , 32 ( 2 ): 129 \u2013 198 , 1977 . G. S. Makanin. The problem of solvability of equations in a free semigroup. Sbornik: Mathematics, 32(2):129\u2013198, 1977.","journal-title":"Mathematics"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/1536616.1536637"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic model checking","author":"McMillan K. L.","year":"1993","unstructured":"K. L. McMillan . Symbolic model checking . Kluwer , 1993 . K. L. McMillan. Symbolic model checking. Kluwer, 1993."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1060745.1060809"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.5555\/646792.704677"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.5555\/795665.796529"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/990308.990312"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/1132516.1132584"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2389836.2389853"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.5555\/1629683"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2011.11.003"},{"key":"e_1_3_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0022-0000(70)80006-X"},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.38"},{"key":"e_1_3_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1145\/2046707.2046776"},{"key":"e_1_3_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-1984-0742421-9"},{"key":"e_1_3_2_1_61_1","volume-title":"PWS Publishing Company","author":"Sipser M.","year":"1997","unstructured":"M. Sipser . Introduction to the Theory of Computation . PWS Publishing Company , 1997 . M. Sipser. Introduction to the Theory of Computation. PWS Publishing Company, 1997."},{"key":"e_1_3_2_1_62_1","first-page":"670","volume-title":"USENIX Security","author":"Stock B.","year":"2014","unstructured":"B. Stock , S. Lekies , T. Mueller , P. Spiegel , and M. Johns . Precise client-side protection against dom-based cross-site scripting . In USENIX Security , pages 655\u2013 670 , 2014 . B. Stock, S. Lekies, T. Mueller, P. Spiegel, and M. Johns. Precise client-side protection against dom-based cross-site scripting. In USENIX Security, pages 655\u2013670, 2014."},{"key":"e_1_3_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12032-9_16"},{"key":"e_1_3_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660372"},{"key":"e_1_3_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103674"},{"key":"e_1_3_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250739"},{"key":"e_1_3_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368112"},{"key":"e_1_3_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390661"},{"key":"e_1_3_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.5555\/2041225.2041237"},{"key":"e_1_3_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_28"},{"key":"e_1_3_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_13"},{"key":"e_1_3_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985828"},{"key":"e_1_3_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054111009112"},{"key":"e_1_3_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-013-0189-1"},{"key":"e_1_3_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491411.2491456"}],"event":{"name":"POPL '16: The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"St. Petersburg FL USA","acronym":"POPL '16","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2837614.2837641","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2837614.2837641","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:43:38Z","timestamp":1750211018000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2837614.2837641"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,11]]},"references-count":74,"alternative-id":["10.1145\/2837614.2837641","10.1145\/2837614"],"URL":"https:\/\/doi.org\/10.1145\/2837614.2837641","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2914770.2837641","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2016,1,11]]},"assertion":[{"value":"2016-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}