{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:34:31Z","timestamp":1750221271533,"version":"3.41.0"},"reference-count":18,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2018,1,11]],"date-time":"2018-01-11T00:00:00Z","timestamp":1515628800000},"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":["SIGSOFT Softw. Eng. Notes"],"published-print":{"date-parts":[[2018,1,11]]},"abstract":"<jats:p>Scaling symbolic execution to industrial-sized programs is an important open research problem. Veritesting is a promising technique that improves scalability by combining the advantages of static symbolic execution with those of dynamic symbolic execution. The goal of veritesting is to reduce the number of paths to explore in symbolic execution by creating formulas describing regions of code using disjunctive formulas. In previous work, veritesting was applied to binary-level symbolic execution.<\/jats:p>\n          <jats:p>Integrating veritesting with Java bytecode presents unique challenges: notably, incorporating non-local control jumps caused by runtime polymorphism, exceptions, native calls, and dynamic class loading. If these language features are not accounted for, we hypothesize that the static code regions described by veritesting are often small and may not lead to substantial reduction in paths. We examine this hypothesis by running a Soot-based static analysis on six large open-source projects used in the Defects4J collection. We find that while veritesting can be applied in thousands of regions, allowing static symbolic execution involving non-local control jumps amplifies the performance improvement obtained from veritesting. We hope to use these insights to support efficient veritesting in Symbolic PathFinder in the near future. Toward this end, we brie y address some engineering challenges to add veritesting into SPF.<\/jats:p>","DOI":"10.1145\/3149485.3149491","type":"journal-article","created":{"date-parts":[[2018,1,12]],"date-time":"2018-01-12T13:49:50Z","timestamp":1515764990000},"page":"1-5","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Veritesting Challenges in Symbolic Execution of Java"],"prefix":"10.1145","volume":"42","author":[{"given":"Vaibhav","family":"Sharma","sequence":"first","affiliation":[{"name":"University of Minnesota, Minneapolis, MN, United States of America"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael W.","family":"Whalen","sequence":"additional","affiliation":[{"name":"University of Minnesota, Minneapolis, MN, United States of America"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephen","family":"McCamant","sequence":"additional","affiliation":[{"name":"University of Minnesota, Minneapolis, MN, United States of America"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Willem","family":"Visser","sequence":"additional","affiliation":[{"name":"University of Stellenbosch, Stellenbosch, South Africa"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,1,11]]},"reference":[{"volume-title":"Ullman","year":"2007","author":"Aho Alfred V","key":"e_1_2_1_1_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_1","DOI":"10.1145\/2568225.2568293"},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.1145\/1985793.1985827"},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.1109\/SP.2012.31"},{"doi-asserted-by":"publisher","key":"e_1_2_1_7_1","DOI":"10.1145\/1065010.1065036"},{"doi-asserted-by":"publisher","key":"e_1_2_1_9_1","DOI":"10.1145\/2635868.2635929"},{"doi-asserted-by":"publisher","key":"e_1_2_1_10_1","DOI":"10.1145\/2254064.2254088"},{"volume-title":"Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis. Automated Software Engineering 20, 3 (01","year":"2013","author":"P\u0103s\u0103reanu Corina S.","key":"e_1_2_1_11_1"},{"volume-title":"Proceedings of the 23rd International Conference on Computer Aided Veri cation (CAV'11)","year":"2032","author":"Ramos David A","key":"e_1_2_1_12_1"},{"unstructured":"McGill University Sable Research Group. 2017a. A Brief Overview Of Shimple. https:\/\/github.com\/Sable\/soot\/wiki\/ A-brief-overview-of-Shimple. (2017).  McGill University Sable Research Group. 2017a. A Brief Overview Of Shimple. https:\/\/github.com\/Sable\/soot\/wiki\/ A-brief-overview-of-Shimple. (2017).","key":"e_1_2_1_13_1"},{"unstructured":"McGill University Sable Research Group. 2017b. Exceptional Unit Graph (Soot API). https:\/\/www.sable.mcgill.ca\/soot\/doc\/soot\/toolkits\/graph\/ExceptionalUnitGraph.html. (2017).  McGill University Sable Research Group. 2017b. Exceptional Unit Graph (Soot API). https:\/\/www.sable.mcgill.ca\/soot\/doc\/soot\/toolkits\/graph\/ExceptionalUnitGraph.html. (2017).","key":"e_1_2_1_14_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_15_1","DOI":"10.1145\/1081706.1081750"},{"doi-asserted-by":"publisher","key":"e_1_2_1_16_1","DOI":"10.1145\/2786805.2786830"},{"volume-title":"Finding Semantically-Equivalent Binary Code By Synthesizing Adaptors. ArXiv e-prints (July","year":"2017","author":"Sharma Vaibhav","key":"e_1_2_1_17_1"},{"volume-title":"2016 IEEE Symposium on Security and Privacy (SP). 138--157","author":"Shoshitaishvili Yan","key":"e_1_2_1_18_1"},{"key":"e_1_2_1_19_1","first-page":"1","article-title":"Driller: Augmenting Fuzzing Through Selective Symbolic Execution","volume":"16","author":"Stephens Nick","year":"2016","journal-title":"NDSS"},{"doi-asserted-by":"publisher","key":"e_1_2_1_20_1","DOI":"10.5555\/781995.782008"},{"doi-asserted-by":"publisher","key":"e_1_2_1_21_1","DOI":"10.1145\/2393596.2393665"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3149485.3149491","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3149485.3149491","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:07Z","timestamp":1750212667000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3149485.3149491"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,11]]},"references-count":18,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2018,1,11]]}},"alternative-id":["10.1145\/3149485.3149491"],"URL":"https:\/\/doi.org\/10.1145\/3149485.3149491","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2018,1,11]]},"assertion":[{"value":"2018-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}