{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:16:14Z","timestamp":1750306574796,"version":"3.41.0"},"reference-count":13,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2015,2,6]],"date-time":"2015-02-06T00:00:00Z","timestamp":1423180800000},"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":[[2015,2,6]]},"abstract":"<jats:p>Symbolic execution is a program analysis technique that is used for many purposes, one of which is test case generation. For loop-free programs, this generates a test set that achieves path coverage. Program loops, however, imply exponential growth of the number of paths in the best case and non-termination in the worst case. In practice, the number of loop unwindings needs to be bounded for analysis.<\/jats:p>\n          <jats:p>We consider symbolic execution in the context of the tool Symbolic Pathfinder. This tool extends the Java Pathfinder model-checker and relies on its bounded state-space exploration for termination. We present an implementation of k-bounded loop un- winding, which increases the amount of user-control over the symbolic execution of loops.<\/jats:p>\n          <jats:p>Bounded unwinding can be viewed as a naive way to prune paths through loops. When using symbolic execution for test case generation, branch coverage will likely be lost when paths are naively pruned. In order to improve coverage of branches within a loop body, we present a technique that semi-automatically concretizes variables used in a loop. The basic technique is limited and we therefore present annotations to manually steer symbolic execution towards certain branches, as well as ideas on how the technique can be extended to be more widely applicable.<\/jats:p>","DOI":"10.1145\/2693208.2693243","type":"journal-article","created":{"date-parts":[[2015,2,10]],"date-time":"2015-02-10T13:19:47Z","timestamp":1423574387000},"page":"1-5","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Improving Coverage of Test Cases Generated by Symbolic PathFinder for Programs with Loops"],"prefix":"10.1145","volume":"40","author":[{"given":"Rody","family":"Kersten","sequence":"first","affiliation":[{"name":"Radboud University, Nijmegen, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Suzette","family":"Person","sequence":"additional","affiliation":[{"name":"NASA Langley RC, Hampton, Virginia, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Neha","family":"Rungta","sequence":"additional","affiliation":[{"name":"NASA Ames RC, Mofett Field, California, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Oksana","family":"Tkachuk","sequence":"additional","affiliation":[{"name":"NASA Ames RC, Mofett Field, California, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2015,2,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"crossref","first-page":"99","DOI":"10.1007\/978-3-642-39176-7_7","volume-title":"Model Checking Software, LNCS 7976","author":"Backes J.","year":"2013"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985995"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2008.22"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2001420.2001424"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050043"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2382756.2382801"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1453101.1453131"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1858996.1859035"},{"key":"e_1_2_1_9_1","first-page":"164","volume-title":"Model Checking Software, LNCS 2989","author":"P\u0103s\u0103reanu C. S.","year":"2004"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSM.2012.6405261"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1572272.1572299"},{"volume-title":"Faculty of Informatics","year":"2013","author":"Trt\u00edk M.","key":"e_1_2_1_12_1"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2013.6693084"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2693208.2693243","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2693208.2693243","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:13:31Z","timestamp":1750227211000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2693208.2693243"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,2,6]]},"references-count":13,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,2,6]]}},"alternative-id":["10.1145\/2693208.2693243"],"URL":"https:\/\/doi.org\/10.1145\/2693208.2693243","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2015,2,6]]},"assertion":[{"value":"2015-02-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}