{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:20:06Z","timestamp":1750306806938,"version":"3.41.0"},"reference-count":13,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2014,2,11]],"date-time":"2014-02-11T00:00:00Z","timestamp":1392076800000},"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":[[2014,2,11]]},"abstract":"<jats:p>To explore the state space of programs with complex user-defined data structures, most symbolic execution engines use the lazy initialization algorithm. Symbolic Pathfinder (SPF) is the symbolic execution engine for the Java PathFinder (JPF) model checker; SPF too contains an implementation of the lazy initialization algorithm. A number of extensions to the original lazy initialization algorithm have since been published. One such extension is the lazier# algorithm which demonstrated dramatic performance gains over the other algorithms. There is, however, no open-source implementation of the lazier# algorithm available. This work is an implementation of the the lazier# algorithm within the Symbolic PathFinder framework. In addition, this work describes the implementation of two heap bounding techniques in SPF, namely k-bounding and n-bounding. The purpose of this paper is to discuss the nature of the improvements, implementation details, usage and performance test results.<\/jats:p>","DOI":"10.1145\/2557833.2560579","type":"journal-article","created":{"date-parts":[[2014,2,18]],"date-time":"2014-02-18T14:08:32Z","timestamp":1392732512000},"page":"1-5","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Towards a lazier symbolic pathfinder"],"prefix":"10.1145","volume":"39","author":[{"given":"Benjamin","family":"Hillery","sequence":"first","affiliation":[{"name":"Brigham Young University, Provo, UT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Eric","family":"Mercer","sequence":"additional","affiliation":[{"name":"Brigham Young University, Provo, UT"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Neha","family":"Rungta","sequence":"additional","affiliation":[{"name":"NASA Ames, Mountain View, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Suzette","family":"Person","sequence":"additional","affiliation":[{"name":"NASA Langley, Hampton, VA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,2,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11537328_2"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/800191.805647"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2006.26"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-011-0089-9"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2007.43"},{"key":"e_1_2_1_6_1","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1007\/978-3-642-38088-4_16","volume-title":"NASA Formal Methods","author":"Geldenhuys J.","year":"2013"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765871.1765924"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1858996.1859035"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1390630.1390635"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081750"},{"volume-title":"Addison-Wesley","year":"1999","author":"Weiss M. A.","key":"e_1_2_1_13_1"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2557833.2560579","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2557833.2560579","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:34:58Z","timestamp":1750232098000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2557833.2560579"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,2,11]]},"references-count":13,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,2,11]]}},"alternative-id":["10.1145\/2557833.2560579"],"URL":"https:\/\/doi.org\/10.1145\/2557833.2560579","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2014,2,11]]},"assertion":[{"value":"2014-02-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}