{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:49:54Z","timestamp":1750308594586,"version":"3.41.0"},"reference-count":13,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2017,1,5]],"date-time":"2017-01-05T00:00:00Z","timestamp":1483574400000},"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":[[2017,1,5]]},"abstract":"<jats:p>Symbolic Execution is a program analysis technique used to increase software reliability. Modern software often manipulate complex data structures, many of which being similar to arrays. We present a novel approach and implementation in Symbolic PathFinder for handling symbolic arrays in Java. It enables analyzing a broader class of programs that manipulates arrays. We also extend the Symbolic Pathfinder testcase generation to support numeric arrays.<\/jats:p>","DOI":"10.1145\/3011286.3011296","type":"journal-article","created":{"date-parts":[[2017,1,6]],"date-time":"2017-01-06T13:30:07Z","timestamp":1483709407000},"page":"1-5","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Symbolic Arrays in Symbolic PathFinder"],"prefix":"10.1145","volume":"41","author":[{"given":"Aymeric","family":"Fromherz","sequence":"first","affiliation":[{"name":"\u00c9cole Normale Sup\u00e9rieure"}]},{"given":"Kasper S.","family":"Luckow","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University"}]},{"given":"Corina S.","family":"P\u0103s\u0103reanu","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, NASA Ames"}]}],"member":"320","published-online":{"date-parts":[[2017,1,5]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/2568225.2568293"},{"volume-title":"ICSE '13","author":"Bounimova E.","key":"e_1_2_1_2_1","unstructured":"E. Bounimova , P. Godefroid , and D. Molnar . Billions and billions of constraints: Whitebox fuzz testing in production . ICSE '13 . E. Bounimova, P. Godefroid, and D. Molnar. Billions and billions of constraints: Whitebox fuzz testing in production. ICSE '13."},{"volume-title":"ICSE'11","author":"Cadar C.","key":"e_1_2_1_3_1","unstructured":"C. Cadar , P. Godefroid , S. Khurshid , C. S. P\u0103s\u0103reanu , K. Sen , N. Tillmann , and W. Visser . Symbolic execution for software testing in practice: Preliminary assessment . ICSE'11 . C. Cadar, P. Godefroid, S. Khurshid, C. S. P\u0103s\u0103reanu, K. Sen, N. Tillmann, and W. Visser. Symbolic execution for software testing in practice: Preliminary assessment. ICSE'11."},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31759-0_19"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1713254.1713257"},{"key":"e_1_2_1_6_1","unstructured":"L. De Moura and N. Bj\u00f8rner. Z3: an efficient smt solver. TACAS'08\/ETAPS'08.  L. De Moura and N. Bj\u00f8rner. Z3: an efficient smt solver. TACAS'08\/ETAPS'08."},{"key":"e_1_2_1_7_1","unstructured":"L. de Moura and N. Bj\u00f8rner. Generalized efficient array decision procedures.  L. de Moura and N. Bj\u00f8rner. Generalized efficient array decision procedures."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36577-X_40"},{"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.1007\/978-3-662-49674-9_26"},{"key":"e_1_2_1_11_1","first-page":"21","volume-title":"In IFIP Congress","author":"Mccarthy J.","year":"1962","unstructured":"J. Mccarthy . Towards a mathematical science of computation . In In IFIP Congress , pages 21 -- 28 . North-Holland , 1962 . J. Mccarthy. Towards a mathematical science of computation. In In IFIP Congress, pages 21--28. North-Holland, 1962."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-013-0122-2"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_26"}],"container-title":["ACM SIGSOFT Software Engineering Notes"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3011286.3011296","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3011286.3011296","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:28Z","timestamp":1750273528000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3011286.3011296"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,1,5]]},"references-count":13,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2017,1,5]]}},"alternative-id":["10.1145\/3011286.3011296"],"URL":"https:\/\/doi.org\/10.1145\/3011286.3011296","relation":{},"ISSN":["0163-5948"],"issn-type":[{"type":"print","value":"0163-5948"}],"subject":[],"published":{"date-parts":[[2017,1,5]]},"assertion":[{"value":"2017-01-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}