{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,29]],"date-time":"2026-04-29T08:07:49Z","timestamp":1777450069625,"version":"3.51.4"},"publisher-location":"New York, NY, USA","reference-count":20,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,11,5]],"date-time":"2018-11-05T00:00:00Z","timestamp":1541376000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000028","name":"Semiconductor Research Corporation","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000028","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,11,5]]},"DOI":"10.1145\/3240765.3240771","type":"proceedings-article","created":{"date-parts":[[2018,11,6]],"date-time":"2018-11-06T13:36:57Z","timestamp":1541511417000},"page":"1-8","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["A formal instruction-level GPU model for scalable verification"],"prefix":"10.1145","author":[{"given":"Yue","family":"Xing","sequence":"first","affiliation":[{"name":"Princeton University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bo-Yuan","family":"Huang","sequence":"additional","affiliation":[{"name":"Princeton University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[{"name":"Princeton University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sharad","family":"Malik","sequence":"additional","affiliation":[{"name":"Princeton University"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2018,11,5]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"GPUDrano: Detecting Uncoalesced Accesses in GPU Programs. In International Conference on Computer Aided Verification. Springer, 507--525","author":"Alur Rajeev","year":"2017","unstructured":"Rajeev Alur, Joseph Devietti, Omar S Navarro Leija, and Nimit Singhania. 2017. GPUDrano: Detecting Uncoalesced Accesses in GPU Programs. In International Conference on Computer Aided Verification. Springer, 507--525."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISPASS.2009.4919648"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2384616.2384625"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Armin Biere Alessandro Cimatti Edmund M Clarke Ofer Strichman Yunshan Zhu et al. 2003. Bounded model checking. Advances in computers 58 11 (2003) 117--148.","DOI":"10.1016\/S0065-2458(03)58003-2"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/IISWC.2009.5306797"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062342"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2007.12"},{"key":"e_1_3_2_1_9_1","volume-title":"A Uniform Specification for System-on-Chip (SoC) Verification. arXiv preprint arXiv:1801.01114","author":"Huang Bo-Yuan","year":"2018","unstructured":"Bo-Yuan Huang, Hongce Zhang, Pramod Subramanyan, Yakir Vizel, Aarti Gupta, and Sharad Malik. 2018. Instruction-Level Abstraction (ILA): A Uniform Specification for System-on-Chip (SoC) Verification. arXiv preprint arXiv:1801.01114 (2018)."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1882291.1882320"},{"key":"e_1_3_2_1_12_1","unstructured":"Nvidia. 2017. CUDA C Programming Guide 9.1. (2017). https:\/\/docs.nvidia.com\/cuda\/cuda-c-programming-guide\/index.html"},{"key":"e_1_3_2_1_13_1","unstructured":"Nvidia. 2017. CUDA Parallel Thread Execution ISA 6.1. (2017). https:\/\/docs.nvidia.com\/cuda\/parallel-thread-execution\/index.html"},{"key":"e_1_3_2_1_14_1","volume-title":"https:\/\/developer.nvidia.com\/cuda-downloads","author":"CUDA","year":"2017","unstructured":"Nvidia. 2017. CUDA Toolkit 9.1. (2017). https:\/\/developer.nvidia.com\/cuda-downloads"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1168857.1168907"},{"key":"e_1_3_2_1_16_1","volume-title":"Template-based Parameterized Synthesis of Uniform Instruction-Level Abstractions for SoC Verification","author":"Subramanyan Pramod","year":"2017","unstructured":"Pramod Subramanyan, Bo-Yuan Huang, Yakir Vizel, Aarti Gupta, and Sharad Malik. 2017. Template-based Parameterized Synthesis of Uniform Instruction-Level Abstractions for SoC Verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (2017)."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2370816.2370865"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2010.5470477"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2038037.1941574"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2013.44"}],"event":{"name":"ICCAD '18: IEEE\/ACM INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN","location":"San Diego California","acronym":"ICCAD '18","sponsor":["IEEE-EDS Electronic Devices Society","IEEE CAS","IEEE CEDA"]},"container-title":["Proceedings of the International Conference on Computer-Aided Design"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3240765.3240771","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3240765.3240771","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:57:32Z","timestamp":1750208252000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3240765.3240771"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,11,5]]},"references-count":20,"alternative-id":["10.1145\/3240765.3240771","10.1145\/3240765"],"URL":"https:\/\/doi.org\/10.1145\/3240765.3240771","relation":{},"subject":[],"published":{"date-parts":[[2018,11,5]]},"assertion":[{"value":"2018-11-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}