{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:20:51Z","timestamp":1776316851276,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":49,"publisher":"ACM","license":[{"start":{"date-parts":[[2015,6,3]],"date-time":"2015-06-03T00:00:00Z","timestamp":1433289600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["FA8750-12-C-0284"],"award-info":[{"award-number":["FA8750-12-C-0284"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1218605, CCF-1318191, CCF-1421575"],"award-info":[{"award-number":["CCF-1218605, CCF-1318191, CCF-1421575"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000003","name":"Boeing","doi-asserted-by":"publisher","award":["Formal Analysis Tools for Cyber Security 2014-2015"],"award-info":[{"award-number":["Formal Analysis Tools for Cyber Security 2014-2015"]}],"id":[{"id":"10.13039\/100000003","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2015,6,3]]},"DOI":"10.1145\/2737924.2737991","type":"proceedings-article","created":{"date-parts":[[2015,6,3]],"date-time":"2015-06-03T11:35:56Z","timestamp":1433331356000},"page":"346-356","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":78,"title":["KJS: a complete formal semantics of JavaScript"],"prefix":"10.1145","author":[{"given":"Daejun","family":"Park","sequence":"first","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Stef\u0103nescu","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Grigore","family":"Ro\u015fu","sequence":"additional","affiliation":[{"name":"University of Illinois at Urbana-Champaign, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,6,3]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"V8 Issue 2243. https:\/\/code.google.com\/p\/v8\/ issues\/detail?id=2243","author":"Arvidsson E.","year":"2012","unstructured":"E. Arvidsson . V8 Issue 2243. https:\/\/code.google.com\/p\/v8\/ issues\/detail?id=2243 , 2012 . Accessed : April 22, 2015. E. Arvidsson. V8 Issue 2243. https:\/\/code.google.com\/p\/v8\/ issues\/detail?id=2243, 2012. Accessed: April 22, 2015."},{"key":"e_1_3_2_1_2_1","first-page":"22","volume-title":"USENIX Security","author":"Bandhakavi S.","unstructured":"S. Bandhakavi , S. T. King , P. Madhusudan , and M. Winslett . VEX: Vetting Browser Extensions for Security Vulnerabilities . In USENIX Security , pages 22\u2013 22 . USENIX, 2010. S. Bandhakavi, S. T. King, P. Madhusudan, and M. Winslett. VEX: Vetting Browser Extensions for Security Vulnerabilities. In USENIX Security, pages 22\u201322. USENIX, 2010."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535876"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676982"},{"key":"e_1_3_2_1_5_1","volume-title":"Accessed","author":"Bruant D.","year":"2015","unstructured":"D. Bruant . ECMAScript Bug 56. https:\/\/bugs.ecmascript.org\/ show_bug.cgi?id=56#c3, 2011 . Accessed : April 22, 2015 . D. Bruant. ECMAScript Bug 56. https:\/\/bugs.ecmascript.org\/ show_bug.cgi?id=56#c3, 2011. Accessed: April 22, 2015."},{"key":"e_1_3_2_1_6_1","volume-title":"Accessed","author":"Bruant D.","year":"2015","unstructured":"D. Bruant . Mozilla Bug 641214. https:\/\/bugzilla.mozilla. org\/show_bug.cgi?id=641214, 2011 . Accessed : April 22, 2015 . D. Bruant. Mozilla Bug 641214. https:\/\/bugzilla.mozilla. org\/show_bug.cgi?id=641214, 2011. Accessed: April 22, 2015."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2047849.2047858"},{"key":"e_1_3_2_1_8_1","volume-title":"O\u2019Reilly Media","author":"Crockford D.","year":"2008","unstructured":"D. Crockford . JavaScript : The Good Parts . O\u2019Reilly Media , 2008 . D. Crockford. JavaScript: The Good Parts. O\u2019Reilly Media, 2008."},{"key":"e_1_3_2_1_9_1","first-page":"337","volume":"4963","author":"de Moura L.","year":"2008","unstructured":"L. de Moura and N. Bj\u00f8rner . Z3: An Efficient SMT Solver. In TACAS , volume 4963 , pages 337 \u2013 340 . LNCS, 2008 . L. de Moura and N. Bj\u00f8rner. Z3: An Efficient SMT Solver. In TACAS, volume 4963, pages 337\u2013340. LNCS, 2008.","journal-title":"Z3: An Efficient SMT Solver. In TACAS"},{"key":"e_1_3_2_1_10_1","volume-title":"https:\/\/mail.mozilla.org\/ pipermail\/es-discuss\/2008-August\/003400.html","author":"Script Harmony Ecma","year":"2008","unstructured":"Ecma TC39. ECMA Script Harmony . https:\/\/mail.mozilla.org\/ pipermail\/es-discuss\/2008-August\/003400.html , 2008 . Accessed : April 22, 2015. Ecma TC39. ECMAScript Harmony. https:\/\/mail.mozilla.org\/ pipermail\/es-discuss\/2008-August\/003400.html, 2008. Accessed: April 22, 2015."},{"key":"e_1_3_2_1_11_1","volume-title":"June","author":"Ecma","year":"2011","unstructured":"Ecma TC39. Standard ECMA-262 ECMAScript Language Specification Edition 5.1 , June 2011 . Ecma TC39. Standard ECMA-262 ECMAScript Language Specification Edition 5.1, June 2011."},{"key":"e_1_3_2_1_12_1","volume-title":"Draft Specification of ECMA-262","author":"Ecma","year":"2014","unstructured":"Ecma TC39. Draft Specification of ECMA-262 6 th Edition. http:\/\/wiki.ecmascript.org\/doku.php?id=harmony: specification_drafts, 2014 . Accessed : April 22, 2015. Ecma TC39. Draft Specification of ECMA-262 6th Edition. http:\/\/wiki.ecmascript.org\/doku.php?id=harmony: specification_drafts, 2014. Accessed: April 22, 2015.","edition":"6"},{"key":"e_1_3_2_1_13_1","volume-title":"TC39 Meeting Minutes. https:\/\/github.com\/ rwaldron\/tc39-notes\/blob\/master\/es6\/2014-09\/sept-23","author":"Ecma","year":"2014","unstructured":"Ecma TC39. TC39 Meeting Minutes. https:\/\/github.com\/ rwaldron\/tc39-notes\/blob\/master\/es6\/2014-09\/sept-23 . md#somehow-we-started-talking-about-test262, 2014 . Ecma TC39. TC39 Meeting Minutes. https:\/\/github.com\/ rwaldron\/tc39-notes\/blob\/master\/es6\/2014-09\/sept-23. md#somehow-we-started-talking-about-test262, 2014."},{"key":"e_1_3_2_1_14_1","volume-title":"April 22","author":"Accessed","year":"2015","unstructured":"Accessed : April 22 , 2015 . Accessed: April 22, 2015."},{"key":"e_1_3_2_1_15_1","volume-title":"Accessed","author":"Ecma","year":"2015","unstructured":"Ecma TC39. Test262 : ECMAScript Language Conformance Test Suite. http:\/\/test262.ecmascript.org, 2014 . Accessed : April 22, 2015 . Ecma TC39. Test262: ECMAScript Language Conformance Test Suite. http:\/\/test262.ecmascript.org, 2014. Accessed: April 22, 2015."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103719"},{"key":"e_1_3_2_1_17_1","first-page":"567","volume":"8586","author":"Filaretti D.","year":"2014","unstructured":"D. Filaretti and S. Maffeis . An Executable Formal Semantics of PHP. In ECOOP , volume 8586 , pages 567 \u2013 592 . LNCS, 2014 . D. Filaretti and S. Maffeis. An Executable Formal Semantics of PHP. In ECOOP, volume 8586, pages 567\u2013592. LNCS, 2014.","journal-title":"An Executable Formal Semantics of PHP. In ECOOP"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429114"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103663"},{"key":"e_1_3_2_1_20_1","volume-title":"Automatically Extracting Requirements Specifications from Natural Language. CoRR, abs\/1403.3142","author":"Ghosh S.","year":"2014","unstructured":"S. Ghosh , D. Elenius , W. Li , P. Lincoln , N. Shankar , and W. Steiner . Automatically Extracting Requirements Specifications from Natural Language. CoRR, abs\/1403.3142 , 2014 . S. Ghosh, D. Elenius, W. Li, P. Lincoln, N. Shankar, and W. Steiner. Automatically Extracting Requirements Specifications from Natural Language. CoRR, abs\/1403.3142, 2014."},{"key":"e_1_3_2_1_21_1","first-page":"168","volume-title":"USENIX Security","author":"Guarnieri S.","unstructured":"S. Guarnieri and B. Livshits . GATEKEEPER: Mostly Static Enforcement of Security and Reliability Policies for Javascript Code . In USENIX Security , pages 151\u2013 168 . USENIX, 2009. S. Guarnieri and B. Livshits. GATEKEEPER: Mostly Static Enforcement of Security and Reliability Policies for Javascript Code. In USENIX Security, pages 151\u2013168. USENIX, 2009."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001442"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1526709.1526785"},{"key":"e_1_3_2_1_24_1","first-page":"126","volume":"6183","author":"Guha A.","year":"2010","unstructured":"A. Guha , C. Saftoiu , and S. Krishnamurthi . The Essence of Javascript. In ECOOP , volume 6183 , pages 126 \u2013 150 . LNCS, 2010 . A. Guha, C. Saftoiu, and S. Krishnamurthi. The Essence of Javascript. In ECOOP, volume 6183, pages 126\u2013150. LNCS, 2010.","journal-title":"The Essence of Javascript. In ECOOP"},{"key":"e_1_3_2_1_25_1","volume-title":"A Formal Semantics of Python 3.3. Master\u2019s thesis","author":"Guth D.","year":"2013","unstructured":"D. Guth . A Formal Semantics of Python 3.3. Master\u2019s thesis , University of Illinois at Urbana-Champaign , July 2013 . D. Guth. A Formal Semantics of Python 3.3. Master\u2019s thesis, University of Illinois at Urbana-Champaign, July 2013."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1292535.1292543"},{"key":"e_1_3_2_1_27_1","volume-title":"Accessed","author":"Herman D.","year":"2015","unstructured":"D. Herman , L. Wagner , and A. Zakai . asm.js. http:\/\/asmjs.org, 2014 . Accessed : April 22, 2015 . D. Herman, L. Wagner, and A. Zakai. asm.js. http:\/\/asmjs.org, 2014. Accessed: April 22, 2015."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2635868.2635904"},{"key":"e_1_3_2_1_29_1","volume-title":"Proceedings of the 2012 International Workshop on Foundations of Object-Oriented Languages. ACM","author":"Lee H.","year":"2012","unstructured":"H. Lee , S. Won , J. Jin , J. Cho , and S. Ryu . SAFE: Formal Specification and Implementation of a Scalable Analysis Framework for ECMAScript . In Proceedings of the 2012 International Workshop on Foundations of Object-Oriented Languages. ACM , 2012 . H. Lee, S. Won, J. Jin, J. Cho, and S. Ryu. SAFE: Formal Specification and Implementation of a Scalable Analysis Framework for ECMAScript. In Proceedings of the 2012 International Workshop on Foundations of Object-Oriented Languages. ACM, 2012."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89330-1_22"},{"key":"e_1_3_2_1_31_1","volume-title":"Accessed","year":"2015","unstructured":"Mean.io. MEAN : A Fullstack Javascript Framework. http:\/\/mean. io\/, 2014 . Accessed : April 22, 2015 . Mean.io. MEAN: A Fullstack Javascript Framework. http:\/\/mean. io\/, 2014. Accessed: April 22, 2015."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37057-1_17"},{"key":"e_1_3_2_1_34_1","volume-title":"Accessed","author":"Orendorff J.","year":"2015","unstructured":"J. Orendorff . Mozilla Bug 779682. https:\/\/bugzilla.mozilla. org\/show_bug.cgi?id=779682, 2012 . Accessed : April 22, 2015 . J. Orendorff. Mozilla Bug 779682. https:\/\/bugzilla.mozilla. org\/show_bug.cgi?id=779682, 2012. Accessed: April 22, 2015."},{"key":"e_1_3_2_1_35_1","unstructured":"D. Park. WebKit Bug 138859 138858; V8 Issue 3704; ECMA-262 Bug 3427 3426; S5 Issues 55 57 59. https:\/\/bugs.webkit.org\/show_bug.cgi?id=138859 https:\/\/bugs.webkit.org\/show_bug.cgi?id=138858 https:\/\/code.google.com\/p\/v8\/issues\/detail?id=3704 https:\/\/bugs.ecmascript.org\/show_bug.cgi?id=3427 https:\/\/bugs.ecmascript.org\/show_bug.cgi?id=3426 https:\/\/github.com\/brownplt\/LambdaS5\/issues\/55 https:\/\/github.com\/brownplt\/LambdaS5\/issues\/57 https:\/\/github.com\/brownplt\/LambdaS5\/issues\/59 2014.  D. Park. WebKit Bug 138859 138858; V8 Issue 3704; ECMA-262 Bug 3427 3426; S5 Issues 55 57 59. https:\/\/bugs.webkit.org\/show_bug.cgi?id=138859 https:\/\/bugs.webkit.org\/show_bug.cgi?id=138858 https:\/\/code.google.com\/p\/v8\/issues\/detail?id=3704 https:\/\/bugs.ecmascript.org\/show_bug.cgi?id=3427 https:\/\/bugs.ecmascript.org\/show_bug.cgi?id=3426 https:\/\/github.com\/brownplt\/LambdaS5\/issues\/55 https:\/\/github.com\/brownplt\/LambdaS5\/issues\/57 https:\/\/github.com\/brownplt\/LambdaS5\/issues\/59 2014."},{"key":"e_1_3_2_1_36_1","volume-title":"April 22","author":"Accessed","year":"2015","unstructured":"Accessed : April 22 , 2015 . Accessed: April 22, 2015."},{"key":"e_1_3_2_1_37_1","volume-title":"Supplementary material. https:\/\/ github.com\/kframework\/javascript-semantics","author":"Park D.","year":"2014","unstructured":"D. Park and A. Stefanescu . Supplementary material. https:\/\/ github.com\/kframework\/javascript-semantics , 2014 . D. Park and A. Stefanescu. Supplementary material. https:\/\/ github.com\/kframework\/javascript-semantics, 2014."},{"key":"e_1_3_2_1_38_1","volume-title":"April 22","author":"Accessed","year":"2015","unstructured":"Accessed : April 22 , 2015 . Accessed: April 22, 2015."},{"key":"e_1_3_2_1_39_1","first-page":"12","volume-title":"USENIX Security","author":"Politz J. G.","unstructured":"J. G. Politz , S. A. Eliopoulos , A. Guha , and S. Krishnamurthi . ADsafety: Type-based Verification of JavaScript Sandboxing . In USENIX Security , pages 12\u2013 12 . USENIX, 2011. J. G. Politz, S. A. Eliopoulos, A. Guha, and S. Krishnamurthi. ADsafety: Type-based Verification of JavaScript Sandboxing. In USENIX Security, pages 12\u201312. USENIX, 2011."},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384577.2384579"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254104"},{"key":"e_1_3_2_1_42_1","volume-title":"An Overview of the K Semantic Framework. Journal of Logic and Algebraic Programming, 79(6): 397\u2013434","author":"Rosu G.","year":"2010","unstructured":"G. Rosu and T. F. Serbanuta . An Overview of the K Semantic Framework. Journal of Logic and Algebraic Programming, 79(6): 397\u2013434 , 2010 . G. Rosu and T. F. Serbanuta. An Overview of the K Semantic Framework. Journal of Logic and Algebraic Programming, 79(6): 397\u2013434, 2010."},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384656"},{"key":"e_1_3_2_1_44_1","volume-title":"Accessed","author":"Samuel M.","year":"2015","unstructured":"M. Samuel . Properties of Interpreters or the Browser Environment that allow Privilege Escalation. https:\/\/code.google.com\/p\/ google-caja\/wiki\/AttackVectors, 2009 . Accessed : April 22, 2015 . M. Samuel. Properties of Interpreters or the Browser Environment that allow Privilege Escalation. https:\/\/code.google.com\/p\/ google-caja\/wiki\/AttackVectors, 2009. Accessed: April 22, 2015."},{"key":"e_1_3_2_1_45_1","volume-title":"Accessed","author":"Samuel M.","year":"2015","unstructured":"M. Samuel . Attack Vectors : Global Object Poisoning. https:\/\/code. google.com\/p\/google-caja\/wiki\/GlobalObjectPoisoning, 2009 . Accessed : April 22, 2015 . M. Samuel. Attack Vectors: Global Object Poisoning. https:\/\/code. google.com\/p\/google-caja\/wiki\/GlobalObjectPoisoning, 2009. Accessed: April 22, 2015."},{"key":"e_1_3_2_1_46_1","first-page":"80","volume-title":"Proceedings of the Second International Workshop on the K Framework and its Applications","volume":"304","author":"Serbanuta T. F.","unstructured":"T. F. Serbanuta , A. Arusoaie , D. Lazar , C. Ellison , D. Lucanu , and G. Rosu . The K Primer (version 3.3) . In Proceedings of the Second International Workshop on the K Framework and its Applications , volume 304 , pages 57\u2013 80 . ENTCS, 2013. T. F. Serbanuta, A. Arusoaie, D. Lazar, C. Ellison, D. Lucanu, and G. Rosu. The K Primer (version 3.3). In Proceedings of the Second International Workshop on the K Framework and its Applications, volume 304, pages 57\u201380. ENTCS, 2013."},{"key":"e_1_3_2_1_47_1","volume-title":"https:\/\/bugs.ecmascript.org\/ show_bug.cgi?id=1444","author":"Smith G.","year":"2013","unstructured":"G. Smith . ECMA-262 Bug 1444. https:\/\/bugs.ecmascript.org\/ show_bug.cgi?id=1444 , 2013 . Accessed : April 22, 2015. G. Smith. ECMA-262 Bug 1444. https:\/\/bugs.ecmascript.org\/ show_bug.cgi?id=1444, 2013. Accessed: April 22, 2015."},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2011.39"},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048147.2048224"}],"event":{"name":"PLDI '15: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Portland OR USA","acronym":"PLDI '15","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"]},"container-title":["Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2737924.2737991","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2737924.2737991","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:16:22Z","timestamp":1750212982000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2737924.2737991"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,6,3]]},"references-count":49,"alternative-id":["10.1145\/2737924.2737991","10.1145\/2737924"],"URL":"https:\/\/doi.org\/10.1145\/2737924.2737991","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2813885.2737991","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2015,6,3]]},"assertion":[{"value":"2015-06-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}