{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:43:55Z","timestamp":1780994635118,"version":"3.54.1"},"reference-count":71,"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-nc\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K008528\/1"],"award-info":[{"award-number":["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":[[2019,1,2]]},"abstract":"<jats:p>We propose a novel, unified approach to the development of compositional symbolic execution tools, bridging the gap between classical symbolic execution and compositional program reasoning based on separation logic. Using this approach, we build JaVerT 2.0, a symbolic analysis tool for JavaScript that follows the language semantics without simplifications. JaVerT 2.0 supports whole-program symbolic testing, verification, and, for the first time, automatic compositional testing based on bi-abduction. The meta-theory underpinning JaVerT 2.0 is developed modularly, streamlining the proofs and informing the implementation. Our explicit treatment of symbolic execution errors allows us to give meaningful feedback to the developer during whole-program symbolic testing and guides the inference of resource of the bi-abductive execution. We evaluate the performance of JaVerT 2.0 on a number of JavaScript data-structure libraries, demonstrating: the scalability of our whole-program symbolic testing; an improvement over the state-of-the-art in JavaScript verification; and the feasibility of automatic compositional testing for JavaScript.<\/jats:p>","DOI":"10.1145\/3290379","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":21,"title":["JaVerT 2.0: compositional symbolic execution for JavaScript"],"prefix":"10.1145","volume":"3","author":[{"given":"Jos\u00e9","family":"Fragoso Santos","sequence":"first","affiliation":[{"name":"Imperial College London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Petar","family":"Maksimovi\u0107","sequence":"additional","affiliation":[{"name":"Imperial College London, UK \/ Mathematical Institute SASA, Serbia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Gabriela","family":"Sampaio","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Philippa","family":"Gardner","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}],"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":"crossref","unstructured":"S. Anand C. S. P\u0103s\u0103reanu and W. Visser. 2007. JPF\u2013SE: A Symbolic Execution Extension to Java PathFinder. In TACAS. 134\u2013138.   S. Anand C. S. P\u0103s\u0103reanu and W. Visser. 2007. JPF\u2013SE: A Symbolic Execution Extension to Java PathFinder. In TACAS. 134\u2013138.","DOI":"10.1007\/978-3-540-71209-1_12"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/3220903.3221139"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3182657"},{"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":"crossref","unstructured":"A. Biere A. Cimatti E. Clarke and Y. Zhu. 1999. Symbolic Model Checking without BDDs. In TACAS. 193\u2013207.   A. Biere A. Cimatti E. Clarke and Y. Zhu. 1999. Symbolic Model Checking without BDDs. In TACAS. 193\u2013207.","DOI":"10.1007\/3-540-49059-0_14"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951937"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/566172.566191"},{"key":"e_1_2_2_8_1","first-page":"209","article-title":"KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs","volume":"8","author":"Cadar C.","year":"2008","journal-title":"OSDI"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1455518.1455522"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985995"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"key":"e_1_2_2_12_1","volume-title":"Infer: An Automatic Program Verifier for Memory Safety of C Programs. In NASA Formal Methods Symposium . 459\u2013465","author":"Calcagno C."},{"key":"e_1_2_2_13_1","volume-title":"Moving Fast with Software Verification. In NASA Formal Methods Symposium. 3\u201311","author":"Calcagno C."},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480917"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049697.2049700"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_19"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.30"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2013.6693074"},{"key":"e_1_2_2_19_1","doi-asserted-by":"crossref","unstructured":"K. Claessen J. Dureg\u00e5rd and M. H. Palka. 2015. Generating Constrained Eandom Data with Uniform Distribution. J. Funct. Program. 25 (2015).  K. Claessen J. Dureg\u00e5rd and M. H. Palka. 2015. Generating Constrained Eandom Data with Uniform Distribution. J. Funct. Program. 25 (2015).","DOI":"10.1017\/S0956796815000143"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/351240.351266"},{"key":"e_1_2_2_21_1","doi-asserted-by":"crossref","unstructured":"E. Clarke D. Kroening and F. Lerda. 2004. A Tool for Checking ANSI-C Programs. In TACAS. 168\u2013176.  E. Clarke D. Kroening and F. Lerda. 2004. A Tool for Checking ANSI-C Programs. In TACAS. 168\u2013176.","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984027"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814308"},{"key":"e_1_2_2_24_1","doi-asserted-by":"crossref","unstructured":"L. De Moura and N. Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In TACAS. 337\u2013340.   L. De Moura and N. Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In TACAS. 337\u2013340.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-011-0089-9"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2007.43"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2345156.2254087"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429104"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449782"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1287624.1287653"},{"key":"e_1_2_2_31_1","volume-title":"The","author":"ECMA","edition":"5"},{"key":"e_1_2_2_32_1","unstructured":"ECMA TC39. 2017. Test262 Test Suite. https:\/\/github.com\/tc39\/test262. (2017).  ECMA TC39. 2017. Test262 Test Suite. https:\/\/github.com\/tc39\/test262. (2017)."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1273463.1273464"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236950.3236956"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158138"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103663"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1376916.1376953"},{"key":"e_1_2_2_38_1","doi-asserted-by":"crossref","unstructured":"J. Geldenhuys N. Aguirre M. F. Frias and W. Visser. 2013. Bounded Lazy Initialization. In NASA Formal Methods. 229\u2013243.  J. Geldenhuys N. Aguirre M. F. Frias and W. Visser. 2013. Bounded Lazy Initialization. In NASA Formal Methods. 229\u2013243.","DOI":"10.1007\/978-3-642-38088-4_16"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190226"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1064978.1065036"},{"key":"e_1_2_2_41_1","first-page":"151","article-title":"Automated Whitebox Fuzz Testing","volume":"8","author":"Godefroid P.","year":"2008","journal-title":"NDSS"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706307"},{"key":"e_1_2_2_43_1","doi-asserted-by":"crossref","unstructured":"M. Harman and P. W. O\u2019Hearn. 2018. From Start-ups to Scale-ups: Opportunities and Open Problems for Static and Dynamic Program Analysis. In SCAM.  M. Harman and P. W. O\u2019Hearn. 2018. From Start-ups to Scale-ups: Opportunities and Open Problems for Static and Dynamic Program Analysis. In SCAM.","DOI":"10.1109\/SCAM.2018.00009"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863553"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/373243.375719"},{"key":"e_1_2_2_46_1","doi-asserted-by":"crossref","unstructured":"B. Jacobs J. Smans P. Philippaerts F. Vogels W. Penninckx and F. Piessens. 2011. VeriFast: A Powerful Sound Predictable Fast Verifier for C and Java. In NASA Formal Methods. 41\u201355.   B. Jacobs J. Smans P. Philippaerts F. Vogels W. Penninckx and F. Piessens. 2011. VeriFast: A Powerful Sound Predictable Fast Verifier for C and Java. In NASA Formal Methods. 41\u201355.","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_2_2_47_1","doi-asserted-by":"crossref","unstructured":"S. Khurshid C. S. P\u02c7as\u02c7areanu and W. Visser. 2003. Generalized Symbolic Execution for Model Checking and Testing. In TACAS . 553\u2013568.   S. Khurshid C. S. P\u02c7as\u02c7areanu and W. Visser. 2003. Generalized Symbolic Execution for Model Checking and Testing. In TACAS . 553\u2013568.","DOI":"10.1007\/3-540-36577-X_40"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_32"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_4"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2635868.2635913"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2007.48"},{"key":"e_1_2_2_52_1","doi-asserted-by":"crossref","unstructured":"H. H. Nguyen C. David S. Qin and W.-N. Chin. 2007. Automated Verification of Shape and Size Properties via Separation Logic. In VMCAI. 251\u2013266.   H. H. Nguyen C. David S. Qin and W.-N. Chin. 2007. Automated Verification of Shape and Size Properties via Separation Logic. In VMCAI. 251\u2013266.","DOI":"10.1007\/978-3-540-69738-1_18"},{"key":"e_1_2_2_53_1","doi-asserted-by":"crossref","unstructured":"H. H. Nguyen V. Kuncak and W.-N. Chin. 2008. Runtime Checking for Separation Logic. In VMCAI. 203\u2013217.   H. H. Nguyen V. Kuncak and W.-N. Chin. 2008. Runtime Checking for Separation Logic. In VMCAI. 203\u2013217.","DOI":"10.1007\/978-3-540-78163-9_19"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209109"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737991"},{"key":"e_1_2_2_56_1","volume-title":"Under-Constrained Symbolic Execution: Correctness Checking for Real Code. In USENIX Security Symposium . 49\u201364","author":"Ramos D. A."},{"key":"e_1_2_2_57_1","unstructured":"J. C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS. 55\u201374.   J. C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS. 55\u201374."},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2015.2389225"},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411286.1411292"},{"key":"e_1_2_2_60_1","unstructured":"M. Santos. 2016. Buckets-JS: A JavaScript Data Structure Library. https:\/\/github.com\/mauriciosantos\/Buckets-JS. (2016).  M. Santos. 2016. Buckets-JS: A JavaScript Data Structure Library. https:\/\/github.com\/mauriciosantos\/Buckets-JS. (2016)."},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.38"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_33"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_38"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786830"},{"key":"e_1_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_42"},{"key":"e_1_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2491978"},{"key":"e_1_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509578.2509586"},{"key":"e_1_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-03542-0_8"},{"key":"e_1_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2017.30"},{"key":"e_1_2_2_71_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\/3290379","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290379","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\/3290379"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":71,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290379"],"URL":"https:\/\/doi.org\/10.1145\/3290379","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"}}]}}