{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,5]],"date-time":"2026-03-05T06:27:58Z","timestamp":1772692078732,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":40,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,6,8]],"date-time":"2019-06-08T00:00:00Z","timestamp":1559952000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K035584\/1"],"award-info":[{"award-number":["EP\/K035584\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2019,6,8]]},"DOI":"10.1145\/3314221.3314645","type":"proceedings-article","created":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T21:02:18Z","timestamp":1559941338000},"page":"425-438","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":26,"title":["Sound regular expression semantics for dynamic symbolic execution of JavaScript"],"prefix":"10.1145","author":[{"given":"Blake","family":"Loring","sequence":"first","affiliation":[{"name":"Royal Holloway University of London, UK"}]},{"given":"Duncan","family":"Mitchell","sequence":"additional","affiliation":[{"name":"Royal Holloway University of London, UK"}]},{"given":"Johannes","family":"Kinder","sequence":"additional","affiliation":[{"name":"Bundeswehr University Munich, Germany"}]}],"member":"320","published-online":{"date-parts":[[2019,6,8]]},"reference":[{"key":"e_1_3_2_2_1_1","volume-title":"Yu-Fang Chen, Lukas Holik, Ahmed Rezine, Philipp Rummer, and Jari Stenman.","author":"Abdulla Parosh Aziz","year":"2015","unstructured":"Parosh Aziz Abdulla , Mohamed Faouzi Atig , Yu-Fang Chen, Lukas Holik, Ahmed Rezine, Philipp Rummer, and Jari Stenman. 2015 . Norn : An SMT Solver for String Constraints. In Computer Aided Verification (CAV) . Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukas Holik, Ahmed Rezine, Philipp Rummer, and Jari Stenman. 2015. Norn: An SMT Solver for String Constraints. In Computer Aided Verification (CAV)."},{"key":"e_1_3_2_2_2_1","volume-title":"Flatten and Conquer: A Framework for Efficient Analysis of String Constraints. In ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI).","author":"Abdulla Parosh Aziz","year":"2017","unstructured":"Parosh Aziz Abdulla , Mohamed Faouzi Atig , Yu-Fang Chen , Bui Phi Diep , Luk\u00e1? Hol\u00edk, Ahmed Rezine , and Philipp R\u00fcmmer . 2017 . Flatten and Conquer: A Framework for Efficient Analysis of String Constraints. In ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI). Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Luk\u00e1? Hol\u00edk, Ahmed Rezine, and Philipp R\u00fcmmer. 2017. Flatten and Conquer: A Framework for Efficient Analysis of String Constraints. In ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI)."},{"key":"e_1_3_2_2_3_1","volume-title":"Handbook of Theoretical Computer Science (Vol. A), Jan van Leeuwen (Ed.)","author":"Aho Alfred V.","unstructured":"Alfred V. Aho . 1990. Algorithms for Finding Patterns in Strings . In Handbook of Theoretical Computer Science (Vol. A), Jan van Leeuwen (Ed.) . MIT Press , 255-300. Alfred V. Aho. 1990. Algorithms for Finding Patterns in Strings. In Handbook of Theoretical Computer Science (Vol. A), Jan van Leeuwen (Ed.). MIT Press, 255-300."},{"key":"e_1_3_2_2_4_1","volume-title":"Demand-driven Compositional Symbolic Execution. In 14th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS).","author":"Anand Saswat","year":"2008","unstructured":"Saswat Anand , Patrice Godefroid , and Nikolai Tillmann . 2008 . Demand-driven Compositional Symbolic Execution. In 14th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Saswat Anand, Patrice Godefroid, and Nikolai Tillmann. 2008. Demand-driven Compositional Symbolic Execution. In 14th Int. Conf. Tools and Algorithms for the Construction and Analysis of Systems (TACAS)."},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568293"},{"key":"e_1_3_2_2_6_1","volume-title":"SMT-LIB Sequences and Regular Expressions. In Int. Workshop on Satisfiability Modulo Theories (SMT).","author":"Bj\u00f8rner Nikolaj","year":"2012","unstructured":"Nikolaj Bj\u00f8rner , Vijay Ganesh , Rapha\u00ebl Michel , and Margus Veanes . 2012 . SMT-LIB Sequences and Regular Expressions. In Int. Workshop on Satisfiability Modulo Theories (SMT). Nikolaj Bj\u00f8rner, Vijay Ganesh, Rapha\u00ebl Michel, and Margus Veanes. 2012. SMT-LIB Sequences and Regular Expressions. In Int. Workshop on Satisfiability Modulo Theories (SMT)."},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"crossref","unstructured":"Nikolaj Bj\u00f8rner Nikolai Tillmann and Andrei Voronkov. 2009. Path Feasibility Analysis for String-Manipulating Programs. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS).   Nikolaj Bj\u00f8rner Nikolai Tillmann and Andrei Voronkov. 2009. Path Feasibility Analysis for String-Manipulating Programs. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS) .","DOI":"10.1007\/978-3-642-00768-2_27"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535876"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"crossref","unstructured":"Stefan Bucur Johannes Kinder and George Candea. 2014. Prototyping symbolic execution engines for interpreted languages. In Architectural Support for Programming Languages and Operating Systems (ASPLOS).   Stefan Bucur Johannes Kinder and George Candea. 2014. Prototyping symbolic execution engines for interpreted languages. In Architectural Support for Programming Languages and Operating Systems (ASPLOS) .","DOI":"10.1145\/2541940.2541977"},{"key":"e_1_3_2_2_10_1","article-title":"A Formal Study of Practical Regular","volume":"14","author":"C\u00e2mpeanu Cezar","year":"2003","unstructured":"Cezar C\u00e2mpeanu , Kai Salomaa , and Sheng Yu . 2003 . A Formal Study of Practical Regular Expressions. Int. J. Foundations of Computer Science 14 , 06 (2003). Cezar C\u00e2mpeanu, Kai Salomaa, and Sheng Yu. 2003. A Formal Study of Practical Regular Expressions. Int. J. Foundations of Computer Science 14, 06 (2003).","journal-title":"Expressions. Int. J. Foundations of Computer Science"},{"key":"e_1_3_2_2_11_1","volume-title":"Exploring Regular Expression Usage and Context in Python. In Int. Symp. on Software Testing and Analysis (ISSTA).","author":"Chapman Carl","unstructured":"Carl Chapman and Kathryn T. Stolee . 2016 . Exploring Regular Expression Usage and Context in Python. In Int. Symp. on Software Testing and Analysis (ISSTA). Carl Chapman and Kathryn T. Stolee. 2016. Exploring Regular Expression Usage and Context in Python. In Int. Symp. on Software Testing and Analysis (ISSTA)."},{"key":"e_1_3_2_2_12_1","volume-title":"POPL","author":"Chen Taolue","year":"2018","unstructured":"Taolue Chen , Yan Chen , Matthew Hague , Anthony W. Lin , and Zhilin Wu. 2018. What is decidable about string constraints with the ReplaceAll function. PACMPL 2 , POPL ( 2018 ), 3:1-3:29. Taolue Chen, Yan Chen, Matthew Hague, Anthony W. Lin, and Zhilin Wu. 2018. What is decidable about string constraints with the ReplaceAll function. PACMPL 2, POPL (2018), 3:1-3:29."},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"crossref","unstructured":"Leonardo Mendon\u00e7a de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS).  Leonardo Mendon\u00e7a de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS) .","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_2_14_1","unstructured":"ECMA International. 2015. ECMAScript 2015 Language Specification.  ECMA International. 2015. ECMAScript 2015 Language Specification ."},{"key":"e_1_3_2_2_15_1","volume-title":"Simple linear string constraints. Formal Asp. Comput. 25, 6","author":"Fu Xiang","year":"2013","unstructured":"Xiang Fu , Michael C. Powell , Michael Bantegui , and Chung-Chih Li. 2013. Simple linear string constraints. Formal Asp. Comput. 25, 6 ( 2013 ). Xiang Fu, Michael C. Powell, Michael Bantegui, and Chung-Chih Li. 2013. Simple linear string constraints. Formal Asp. Comput. 25, 6 (2013)."},{"key":"e_1_3_2_2_16_1","volume-title":"Compositional Dynamic Test Generation. In ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL).","author":"Godefroid Patrice","year":"2007","unstructured":"Patrice Godefroid . 2007 . Compositional Dynamic Test Generation. In ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL). Patrice Godefroid. 2007. Compositional Dynamic Test Generation. In ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages (POPL)."},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_3_2_2_18_1","volume-title":"Automated Whitebox Fuzz Testing. In Network and Distributed System Security Symp. (NDSS).","author":"Godefroid Patrice","year":"2008","unstructured":"Patrice Godefroid , Michael Levin , and David Molnar . 2008 . Automated Whitebox Fuzz Testing. In Network and Distributed System Security Symp. (NDSS). Patrice Godefroid, Michael Levin, and David Molnar. 2008. Automated Whitebox Fuzz Testing. In Network and Distributed System Security Symp. (NDSS)."},{"key":"e_1_3_2_2_19_1","volume-title":"DLint: Dynamically Checking Bad Coding Practices in JavaScript. In Int. Symp. on Software Testing and Analysis (ISSTA).","author":"Gong Liang","year":"2015","unstructured":"Liang Gong , Michael Pradel , Manu Sridharan , and Koushik Sen . 2015 . DLint: Dynamically Checking Bad Coding Practices in JavaScript. In Int. Symp. on Software Testing and Analysis (ISSTA). Liang Gong, Michael Pradel, Manu Sridharan, and Koushik Sen. 2015. DLint: Dynamically Checking Bad Coding Practices in JavaScript. In Int. Symp. on Software Testing and Analysis (ISSTA)."},{"key":"e_1_3_2_2_20_1","volume-title":"POPL","author":"Hol\u00edk Luk\u00e1s","year":"2018","unstructured":"Luk\u00e1s Hol\u00edk , Petr Janku , Anthony W. Lin , Philipp R\u00fcmmer , and Tom\u00e1s Vojnar . 2018. String constraints with concatenation and transducers solved efficiently. PACMPL 2 , POPL ( 2018 ), 4:1-4:32. Luk\u00e1s Hol\u00edk, Petr Janku, Anthony W. Lin, Philipp R\u00fcmmer, and Tom\u00e1s Vojnar. 2018. String constraints with concatenation and transducers solved efficiently. PACMPL 2, POPL (2018), 4:1-4:32."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254088"},{"key":"e_1_3_2_2_22_1","unstructured":"Guodong Li Esben Andreasen and Indradeep Ghosh. 2014. SymJS: automatic symbolic testing of JavaScript web applications. In Foundations of Software Engineering (FSE).   Guodong Li Esben Andreasen and Indradeep Ghosh. 2014. SymJS: automatic symbolic testing of JavaScript web applications. In Foundations of Software Engineering (FSE) ."},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03077-7_2"},{"key":"e_1_3_2_2_24_1","volume-title":"Reggae: Automated test generation for programs using complex regular expressions. In Automated Software Engineering (ASE).","author":"Li Nuo","year":"2009","unstructured":"Nuo Li , Tao Xie , Nikolai Tillmann , Jonathan de Halleux , and Wolfram Schulte . 2009 . Reggae: Automated test generation for programs using complex regular expressions. In Automated Software Engineering (ASE). Nuo Li, Tao Xie, Nikolai Tillmann, Jonathan de Halleux, and Wolfram Schulte. 2009. Reggae: Automated test generation for programs using complex regular expressions. In Automated Software Engineering (ASE)."},{"key":"e_1_3_2_2_25_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 Computer Aided Verification (CAV).   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 Computer Aided Verification (CAV) .","DOI":"10.1007\/978-3-319-08867-9_43"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24246-0_9"},{"key":"e_1_3_2_2_27_1","volume-title":"ExpoSE: Practical Symbolic Execution of Standalone JavaScript. In Int. SPIN Symp. on Model Checking Software (SPIN).","author":"Loring Blake","year":"2017","unstructured":"Blake Loring , Duncan Mitchell , and Johannes Kinder . 2017 . ExpoSE: Practical Symbolic Execution of Standalone JavaScript. In Int. SPIN Symp. on Model Checking Software (SPIN). Blake Loring, Duncan Mitchell, and Johannes Kinder. 2017. ExpoSE: Practical Symbolic Execution of Standalone JavaScript. In Int. SPIN Symp. on Model Checking Software (SPIN)."},{"key":"e_1_3_2_2_28_1","volume-title":"KJS: A Complete Formal Semantics of JavaScript. In ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI).","author":"Park Daejun","year":"2015","unstructured":"Daejun Park , Andrei Stef?nescu, and Grigore Ro\u00feu . 2015 . KJS: A Complete Formal Semantics of JavaScript. In ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI). Daejun Park, Andrei Stef?nescu, and Grigore Ro\u00feu. 2015. KJS: A Complete Formal Semantics of JavaScript. In ACM SIGPLAN Conf. Programming Language Design and Implementation (PLDI)."},{"key":"e_1_3_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.38"},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"crossref","unstructured":"Joseph D. Scott Pierre Flener and Justin Pearson. 2015. Constraint Solving on Bounded String Variables. In Integration of AI and OR Tech. in Constraint Prog. (CPAIOR).  Joseph D. Scott Pierre Flener and Justin Pearson. 2015. Constraint Solving on Bounded String Variables. In Integration of AI and OR Tech. in Constraint Prog. (CPAIOR) .","DOI":"10.1007\/978-3-319-18008-3_26"},{"key":"e_1_3_2_2_31_1","unstructured":"Koushik Sen Swaroop Kalasapur Tasneem Brutch and Simon Gibbs. 2013. Jalangi: a selective record-replay and dynamic analysis framework for JavaScript. In Foundations of Software Engineering (FSE).   Koushik Sen Swaroop Kalasapur Tasneem Brutch and Simon Gibbs. 2013. Jalangi: a selective record-replay and dynamic analysis framework for JavaScript. In Foundations of Software Engineering (FSE) ."},{"key":"e_1_3_2_2_32_1","volume-title":"Int. Conf. Software Engineering (ICSE).","author":"Thom\u00e9 Julian","unstructured":"Julian Thom\u00e9 , Lwin Khin Shar , Domenico Bianculli , and Lionel C. Briand . 2017. Search-driven string constraint solving for vulnerability detection . In Int. Conf. Software Engineering (ICSE). Julian Thom\u00e9, Lwin Khin Shar, Domenico Bianculli, and Lionel C. Briand. 2017. Search-driven string constraint solving for vulnerability detection. In Int. Conf. Software Engineering (ICSE)."},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"crossref","unstructured":"Nikolai Tillmann and Wolfram Schulte. 2005. Parameterized unit tests. In Foundations of Software Engineering (FSE).   Nikolai Tillmann and Wolfram Schulte. 2005. Parameterized unit tests. In Foundations of Software Engineering (FSE) .","DOI":"10.1145\/1081706.1081745"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660267.2660372"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"crossref","unstructured":"Minh-Thai Trinh Duc-Hiep Chu and Joxan Jaffar. 2016. Progressive Reasoning over Recursively-Defined Strings. In Computer Aided Verification (CAV).  Minh-Thai Trinh Duc-Hiep Chu and Joxan Jaffar. 2016. Progressive Reasoning over Recursively-Defined Strings. In Computer Aided Verification (CAV) .","DOI":"10.1007\/978-3-319-41528-4_12"},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"crossref","unstructured":"Minh-Thai Trinh Duc-Hiep Chu and Joxan Jaffar. 2017. Model Counting for Recursively-Defined Strings. In Computer Aided Verification (CAV).  Minh-Thai Trinh Duc-Hiep Chu and Joxan Jaffar. 2017. Model Counting for Recursively-Defined Strings. In Computer Aided Verification (CAV) .","DOI":"10.1007\/978-3-319-63390-9_21"},{"key":"e_1_3_2_2_37_1","volume-title":"Rex: Symbolic regular expression explorer. In Software Testing, Verification and Validation (ICST).","author":"Veanes Margus","year":"2010","unstructured":"Margus Veanes , Peli de Halleux , and Nikolai Tillmann . 2010 . Rex: Symbolic regular expression explorer. In Software Testing, Verification and Validation (ICST). Margus Veanes, Peli de Halleux, and Nikolai Tillmann. 2010. Rex: Symbolic regular expression explorer. In Software Testing, Verification and Validation (ICST)."},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0263-6"},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"crossref","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 (CAV).  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 (CAV) .","DOI":"10.1007\/978-3-319-21690-4_14"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"crossref","unstructured":"Yunhui Zheng Xiangyu Zhang and Vijay Ganesh. 2013. Z3-str: A Z3-based String Solver for Web Application Analysis. In Foundations of Software Engineering (FSE).   Yunhui Zheng Xiangyu Zhang and Vijay Ganesh. 2013. Z3-str: A Z3-based String Solver for Web Application Analysis. In Foundations of Software Engineering (FSE) .","DOI":"10.1145\/2491411.2491456"}],"event":{"name":"PLDI '19: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Phoenix AZ USA","acronym":"PLDI '19","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314645","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3314221.3314645","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T23:53:29Z","timestamp":1750204409000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3314221.3314645"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,6,8]]},"references-count":40,"alternative-id":["10.1145\/3314221.3314645","10.1145\/3314221"],"URL":"https:\/\/doi.org\/10.1145\/3314221.3314645","relation":{},"subject":[],"published":{"date-parts":[[2019,6,8]]},"assertion":[{"value":"2019-06-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}