{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,13]],"date-time":"2026-06-13T09:09:37Z","timestamp":1781341777452,"version":"3.54.1"},"publisher-location":"New York, NY, USA","reference-count":38,"publisher":"ACM","license":[{"start":{"date-parts":[[2014,6,9]],"date-time":"2014-06-09T00:00:00Z","timestamp":1402272000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000015","name":"U.S. Department of Energy","doi-asserted-by":"publisher","award":["DOE DE-SC0005136, DOE FOA-0000619"],"award-info":[{"award-number":["DOE DE-SC0005136, DOE FOA-0000619"]}],"id":[{"id":"10.13039\/100000015","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100002418","name":"Intel Corporation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100002418","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100004356","name":"Nokia","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100004356","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["NSF CCF-0916351, NSF CCF-1139138, NSF CCF-1337415"],"award-info":[{"award-number":["NSF CCF-0916351, NSF CCF-1139138, NSF CCF-1337415"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100004358","name":"Samsung","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100004358","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2014,6,9]]},"DOI":"10.1145\/2594291.2594340","type":"proceedings-article","created":{"date-parts":[[2014,5,13]],"date-time":"2014-05-13T08:18:34Z","timestamp":1399969114000},"page":"530-541","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":122,"title":["A lightweight symbolic virtual machine for solver-aided host languages"],"prefix":"10.1145","author":[{"given":"Emina","family":"Torlak","sequence":"first","affiliation":[{"name":"U.C. Berkeley"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Rastislav","family":"Bodik","sequence":"additional","affiliation":[{"name":"U.C. Berkeley"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2014,6,9]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"http:\/\/developer.amd.com\/tools-and-sdks\/heterogeneous-computing\/amd-accelerated-parallel-processing-app-sdk\/samples-demos\/","author":"Samples AMD.","year":"2013","unstructured":"AMD. Samples & demos. http:\/\/developer.amd.com\/tools-and-sdks\/heterogeneous-computing\/amd-accelerated-parallel-processing-app-sdk\/samples-demos\/ , 2013 . AMD. Samples & demos. http:\/\/developer.amd.com\/tools-and-sdks\/heterogeneous-computing\/amd-accelerated-parallel-processing-app-sdk\/samples-demos\/, 2013."},{"key":"e_1_3_2_1_2_1","volume-title":"Algorithms, Source Code","author":"Arndt J.","year":"2011","unstructured":"J. Arndt . Matters Computational: Ideas , Algorithms, Source Code . Springer , 2011 . J. Arndt. Matters Computational: Ideas, Algorithms, Source Code. Springer, 2011."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/1368088.1368118"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1108792.1108813"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30569-9_3"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2408776.2408795"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1180405.1180445"},{"key":"e_1_3_2_1_9_1","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 , 2008 . C. Cadar, D. Dunbar, and D. Engler. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In OSDI, 2008."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985811"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146251"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/1287624.1287653"},{"key":"e_1_3_2_1_17_1","volume-title":"CAV","author":"Filli\u00e2tre J. C.","year":"2007","unstructured":"J. C. Filli\u00e2tre and C. March\u00e9 . The Why\/Krakatoa\/Caduceus platform for deductive program verification . In CAV , 2007 . J. C. Filli\u00e2tre and C. March\u00e9. The Why\/Krakatoa\/Caduceus platform for deductive program verification. In CAV, 2007."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500574"},{"key":"e_1_3_2_1_20_1","volume-title":"CAV","author":"Jose M.","year":"2011","unstructured":"M. Jose and R. Majumdar . Bug-Assist: assisting fault localization in ANSI-C programs . In CAV , 2011 . M. Jose and R. Majumdar. Bug-Assist: assisting fault localization in ANSI-C programs. In CAV, 2011."},{"key":"e_1_3_2_1_21_1","volume-title":"November","author":"Specification The","year":"2012","unstructured":"The OpenCL Specification , Version 1.2. Khronos OpenCL Working Group , November 2012 . The OpenCL Specification, Version 1.2. Khronos OpenCL Working Group, November 2012."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1765871.1765924"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/319838.319859"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103675"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429125"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796805005733"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2254064.2254088"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_26"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2393596.2393667"},{"key":"e_1_3_2_1_32_1","unstructured":"Racket. The Racket programming language. racket-lang.org.  Racket. The Racket programming language. racket-lang.org."},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/1039991.1039992"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/243753.243762"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.38"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27705-4_11"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/647165.717851"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2509578.2509586"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806635"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/1232420.1232423"}],"event":{"name":"PLDI '14: ACM SIGPLAN Conference on Programming Language Design and Implementation","location":"Edinburgh United Kingdom","acronym":"PLDI '14","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery","NSF"]},"container-title":["Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2594291.2594340","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2594291.2594340","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:56:02Z","timestamp":1750215362000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2594291.2594340"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,6,9]]},"references-count":38,"alternative-id":["10.1145\/2594291.2594340","10.1145\/2594291"],"URL":"https:\/\/doi.org\/10.1145\/2594291.2594340","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2666356.2594340","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2014,6,9]]},"assertion":[{"value":"2014-06-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}