{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:25:02Z","timestamp":1750307102319,"version":"3.41.0"},"reference-count":35,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2012,11,27]],"date-time":"2012-11-27T00:00:00Z","timestamp":1353974400000},"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":[[2012,11,27]]},"abstract":"<jats:p>Recently, symbolic execution has gained a significant progress in its techniques and applications. However, in practice, scalability is still a key challenge for symbolic execution. In this paper, we present S2PF, which improves the scalability of Symbolic PathFinder by integrating speculative symbolic execution with the general heuristic search framework. In addition, two optimizations are proposed to improve the speculative symbolic execution in S2PF. Experimental results on six programs show that, S2PF can reduce the solver invocations by 36.4% to 48.7% (with an average of 40.3%), and save the search time by 30.6% to 43.5% (with an average of 35%).<\/jats:p>","DOI":"10.1145\/2382756.2382792","type":"journal-article","created":{"date-parts":[[2012,11,29]],"date-time":"2012-11-29T15:02:27Z","timestamp":1354201347000},"page":"1-5","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["S2PF"],"prefix":"10.1145","volume":"37","author":[{"given":"Yufeng","family":"Zhang","sequence":"first","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}]},{"given":"Zhenbang","family":"Chen","sequence":"additional","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}]},{"given":"Ji","family":"Wang","sequence":"additional","affiliation":[{"name":"National University of Defense Technology, Changsha, China"}]}],"member":"320","published-online":{"date-parts":[[2012,11,27]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-008-0090-1"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2009.15"},{"key":"e_1_2_1_3_1","first-page":"298","volume-title":"CAV","author":"Barrett C.","year":"2007","unstructured":"C. Barrett and C. Tinelli . Cvc3 . In CAV , pages 298 -- 302 , 2007 . C. Barrett and C. Tinelli. Cvc3. In CAV, pages 298--302, 2007."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_28"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34188-5_7"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2008.69"},{"key":"e_1_2_1_7_1","first-page":"209","volume-title":"OSDI","author":"Cadar C.","year":"2008","unstructured":"C. Cadar , D. Dunbar , and D. Engler . Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs . In OSDI , pages 209 -- 224 , 2008 . C. Cadar, D. Dunbar, and D. Engler. Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI, pages 209--224, 2008."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1455518.1455522"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1287\/ijoc.3.2.157"},{"key":"e_1_2_1_10_1","volume-title":"HotDep","author":"Chipounov V.","year":"2009","unstructured":"V. Chipounov , V. Georgescu , C. Zamfir , and G. Candea . Selective symbolic execution . In HotDep , 2009 . V. Chipounov, V. Georgescu, C. Zamfir, and G. Candea. Selective symbolic execution. In HotDep, 2009."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1961295.1950396"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1768142.1768174"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/2016945.2016964"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1713254.1713257"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190226"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/1064978.1065036"},{"key":"e_1_2_1_18_1","volume-title":"NDSS","author":"Godefroid P.","year":"2008","unstructured":"P. Godefroid , M. Levin , D. Molnar , Automated whitebox fuzz testing . In NDSS , 2008 . P. Godefroid, M. Levin, D. Molnar, et al. Automated whitebox fuzz testing. In NDSS, 2008."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/0743-1066(93)90018-C"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-29860-8_32"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/11537328_12"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1572272.1572286"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254088"},{"key":"e_1_2_1_25_1","volume-title":"Artificial intelligence: Structures and strategies for complex problem solving","author":"Luger G.","year":"2005","unstructured":"G. Luger . Artificial intelligence: Structures and strategies for complex problem solving . Addison-Wesley Longman , 2005 . G. Luger. Artificial intelligence: Structures and strategies for complex problem solving. Addison-Wesley Longman, 2005."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1858996.1859035"},{"key":"e_1_2_1_27_1","unstructured":"S2E. https:\/\/s2e.ep.ch\/.  S2E. https:\/\/s2e.ep.ch\/."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081750"},{"key":"e_1_2_1_29_1","first-page":"135","volume-title":"ISCA","author":"Smith J. E.","year":"1981","unstructured":"J. E. Smith . A study of branch prediction strategies . In ISCA , pages 135 -- 148 , 1981 . J. E. Smith. A study of branch prediction strategies. In ISCA, pages 135--148, 1981."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1831708.1831732"},{"key":"e_1_2_1_31_1","first-page":"134","volume-title":"TAP","author":"Tillmann N.","year":"2008","unstructured":"N. Tillmann and J. De Halleux . Pex-white box test generation for. net . In TAP , pages 134 -- 153 , 2008 . N. Tillmann and J. De Halleux. Pex-white box test generation for. net. In TAP, pages 134--153, 2008."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022920129859"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1966445.1966467"},{"key":"e_1_2_1_34_1","unstructured":"Yices. http:\/\/yices.csl.sri.com\/.  Yices. http:\/\/yices.csl.sri.com\/."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISSRE.2012.8"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2382756.2382792","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2382756.2382792","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:34:54Z","timestamp":1750239294000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2382756.2382792"}},"subtitle":["speculative symbolic PathFinder"],"short-title":[],"issued":{"date-parts":[[2012,11,27]]},"references-count":35,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2012,11,27]]}},"alternative-id":["10.1145\/2382756.2382792"],"URL":"https:\/\/doi.org\/10.1145\/2382756.2382792","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2012,11,27]]},"assertion":[{"value":"2012-11-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}