{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,13]],"date-time":"2026-04-13T23:16:43Z","timestamp":1776122203692,"version":"3.50.1"},"reference-count":53,"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:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K032089\/1, EP\/K008528\/1"],"award-info":[{"award-number":["EP\/K032089\/1, EP\/K008528\/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 dynamic nature of JavaScript and its complex semantics make it a difficult target for logic-based verification. We introduce JaVerT, a semi-automatic JavaScript Verification Toolchain, based on separation logic and aimed at the specialist developer wanting rich, mechanically verified specifications of critical JavaScript code. To specify JavaScript programs, we design abstractions that capture its key heap structures (for example, prototype chains and function closures), allowing the developer to write clear and succinct specifications with minimal knowledge of the JavaScript internals. To verify JavaScript programs, we develop JaVerT, a verification pipeline consisting of: JS-2-JSIL, a well-tested compiler from JavaScript to JSIL, an intermediate goto language capturing the fundamental dynamic features of JavaScript; JSIL Verify, a semi-automatic verification tool based on a sound JSIL separation logic; and verified axiomatic specifications of the JavaScript internal functions. Using JaVerT, we verify functional correctness properties of: data-structure libraries (key-value map, priority queue) written in an object-oriented style; operations on data structures such as binary search trees (BSTs) and lists; examples illustrating function closures; and test cases from the official ECMAScript test suite. The verification times suggest that reasoning about larger, more complex code using JaVerT is feasible.<\/jats:p>","DOI":"10.1145\/3158138","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-33","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["JaVerT: JavaScript verification toolchain"],"prefix":"10.1145","volume":"2","author":[{"given":"Jos\u00e9","family":"Fragoso Santos","sequence":"first","affiliation":[{"name":"Imperial College London, UK"}]},{"given":"Petar","family":"Maksimovi\u0107","sequence":"additional","affiliation":[{"name":"Imperial College London, UK \/ Mathematical Institute SASA, Serbia"}]},{"given":"Daiva","family":"Naud\u017ei\u016bnien\u0117","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}]},{"given":"Thomas","family":"Wood","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}]},{"given":"Philippa","family":"Gardner","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11531142_19"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660214"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11679219_9"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_5"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_11"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(4:1)2012"},{"key":"e_1_2_2_9_1","volume-title":"Proceedings of the 2014 ACM International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA 2014, part of SPLASH 2014","author":"Andrew","year":"2014"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535876"},{"key":"e_1_2_2_11_1","volume-title":"Engler","author":"Cadar Cristian","year":"2008"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-17524-9_1"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049697.2049700"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10936-7_9"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984027"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75280"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449782"},{"key":"e_1_2_2_19_1","volume-title":"The","author":"ECMAScript Committee","edition":"5"},{"key":"e_1_2_2_20_1","unstructured":"Facebook. 2017. react.js: A JavaScript Library for Building User Interfaces. https:\/\/facebook.github.io\/react\/ .  Facebook. 2017. react.js: A JavaScript Library for Building User Interfaces. https:\/\/facebook.github.io\/react\/ ."},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660215"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606621"},{"key":"e_1_2_2_23_1","volume-title":"JavaScript: The Definitive Guide","author":"Flanagan David","edition":"3"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1653662.1653715"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429114"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63046-5_2"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103663"},{"key":"e_1_2_2_28_1","unstructured":"Google. 2017. The V8 JavaScript Engine. https:\/\/v8project.blogspot.ie\/ .  Google. 2017. The V8 JavaScript Engine. https:\/\/v8project.blogspot.ie\/ ."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14107-2_7"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1529282.1529711"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_17"},{"key":"e_1_2_2_33_1","unstructured":"Jason Jones. 2016. Priority Queue Data Structure. https:\/\/github.com\/jasonsjones\/queue- pri .  Jason Jones. 2016. Priority Queue Data Structure. https:\/\/github.com\/jasonsjones\/queue- pri ."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676980"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2635868.2635904"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009855"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"e_1_2_2_38_1","volume-title":"Proceedings of the 19th International Workshop on Foundations of Object-Oriented Languages (FOOL","author":"Lee Hongki","year":"2012"},{"key":"e_1_2_2_39_1","unstructured":"Ben Livshits. 2014. JSIR An Intermediate Representation for JavaScript Analysis. http:\/\/too4words.github.io\/jsir\/ .  Ben Livshits. 2014. JSIR An Intermediate Representation for JavaScript Analysis. http:\/\/too4words.github.io\/jsir\/ ."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2015.735"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737991"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040326"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328451"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384577.2384579"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47958-3_21"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676971"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31057-7_20"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491978"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31987-0_28"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509578.2509586"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594340"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_36"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158138","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158138","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\/3158138"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":53,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158138"],"URL":"https:\/\/doi.org\/10.1145\/3158138","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"}}]}}