{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,19]],"date-time":"2026-06-19T02:18:07Z","timestamp":1781835487887,"version":"3.54.5"},"publisher-location":"New York, NY, USA","reference-count":32,"publisher":"ACM","license":[{"start":{"date-parts":[[2008,7,20]],"date-time":"2008-07-20T00:00:00Z","timestamp":1216512000000},"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":[],"published-print":{"date-parts":[[2008,7,20]]},"DOI":"10.1145\/1390630.1390635","type":"proceedings-article","created":{"date-parts":[[2008,7,22]],"date-time":"2008-07-22T13:46:39Z","timestamp":1216734399000},"page":"15-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":176,"title":["Combining unit-level symbolic execution and system-level concrete execution for testing nasa software"],"prefix":"10.1145","author":[{"given":"Corina S.","family":"P\u01ces\u01cereanu","sequence":"first","affiliation":[{"name":"NASA Ames Research Center, Moffett Field, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter C.","family":"Mehlitz","sequence":"additional","affiliation":[{"name":"NASA Ames research Center, Moffett Field, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David H.","family":"Bushnell","sequence":"additional","affiliation":[{"name":"NASA Ames Research Center, Moffett Field, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Karen","family":"Gundy-Burlet","sequence":"additional","affiliation":[{"name":"NASA Ames Research Center, Moffett Field, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael","family":"Lowry","sequence":"additional","affiliation":[{"name":"NASA Ames Research Center, Moffett Field, CA, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Suzette","family":"Person","sequence":"additional","affiliation":[{"name":"University of Nebraska, Lincoln, NE, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mark","family":"Pape","sequence":"additional","affiliation":[{"name":"NASA Johnson Space Center, Houston, TX, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2008,7,20]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.2514\/6.2007-6888"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/552895.857366"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2006.13"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763507.1763522"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763507.1763523"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503274"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.5555\/998675.999437"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1180405.1180445"},{"key":"e_1_3_2_1_10_1","unstructured":"The Choco Constraint Solver. http:\/\/choco.sourceforge.net\/  The Choco Constraint Solver. http:\/\/choco.sourceforge.net\/"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1976.233817"},{"key":"e_1_3_2_1_12_1","unstructured":"The Daikon invariant detector. http:\/\/groups.csail.mit.edu\/pag\/daikon\/\/  The Daikon invariant detector. http:\/\/groups.csail.mit.edu\/pag\/daikon\/\/"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181806"},{"key":"e_1_3_2_1_15_1","volume-title":"Addison--Wesley","author":"Gamma E.","year":"1994","unstructured":"E. Gamma , R. Helm , R. Johnson , and J. M. Vlissides . Design Patterns: Elements of Reusable Object--Oriented Software . Addison--Wesley , 1994 . E. Gamma, R. Helm, R. Johnson, and J. M. Vlissides. Design Patterns: Elements of Reusable Object--Oriented Software. Addison--Wesley, 1994."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/318773.318939"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263717"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065036"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181790"},{"key":"e_1_3_2_1_20_1","volume-title":"Proc. 3rd International Workshop on Formal Approaches to Testing of Software (FATES)","author":"Heimdahl M. P. E.","year":"2003","unstructured":"M. P. E. Heimdahl , S. Rayadurgam , W. Visser , D. George , and J. Gao . Auto-generating test sequences using model checkers: A case study . In Proc. 3rd International Workshop on Formal Approaches to Testing of Software (FATES) , Montreal, Canada , Oct. 2003 . M. P. E. Heimdahl, S. Rayadurgam, W. Visser, D. George, and J. Gao. Auto-generating test sequences using model checkers: A case study. In Proc. 3rd International Workshop on Formal Approaches to Testing of Software (FATES), Montreal, Canada, Oct. 2003."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/1767111.1767128"},{"key":"e_1_3_2_1_22_1","volume-title":"Addison--Wesley","author":"Holzmann G.","year":"2003","unstructured":"G. Holzmann . The Spin Model Checker : Primer and Reference Manual . Addison--Wesley , 2003 . G. Holzmann. The Spin Model Checker: Primer and Reference Manual. Addison--Wesley, 2003."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/646486.694621"},{"key":"e_1_3_2_1_24_1","unstructured":"IASolver. http:\/\/www.cs.brandeis.edu\/~tim\/Applets\/IAsolver.html  IASolver. http:\/\/www.cs.brandeis.edu\/~tim\/Applets\/IAsolver.html"},{"key":"e_1_3_2_1_25_1","unstructured":"Java PathFinder. http:\/\/javapathfinder.sourceforge.net  Java PathFinder. http:\/\/javapathfinder.sourceforge.net"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765871.1765924"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/647169.718161"},{"key":"e_1_3_2_1_29_1","volume-title":"Java(\u2122) Virtual Machine Specification","author":"Lindholm T.","year":"1999","unstructured":"T. Lindholm and F. Yellin . Java(\u2122) Virtual Machine Specification . Prentice Hall , 1999 . T. Lindholm and F. Yellin. Java(\u2122) Virtual Machine Specification. Prentice Hall, 1999."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2003.1244531"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1081706.1081750"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146243"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31980-1_24"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146255"}],"event":{"name":"ISSTA '08: International Symposium on Software Testing and Analysis","location":"Seattle WA USA","acronym":"ISSTA '08","sponsor":["ACM Association for Computing Machinery","SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 2008 international symposium on Software testing and analysis"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1390630.1390635","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1390630.1390635","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T14:47:15Z","timestamp":1750258035000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1390630.1390635"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,7,20]]},"references-count":32,"alternative-id":["10.1145\/1390630.1390635","10.1145\/1390630"],"URL":"https:\/\/doi.org\/10.1145\/1390630.1390635","relation":{},"subject":[],"published":{"date-parts":[[2008,7,20]]},"assertion":[{"value":"2008-07-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}