{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:40:09Z","timestamp":1750207209376,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":10,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,2,14]],"date-time":"2019-02-14T00:00:00Z","timestamp":1550102400000},"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":[[2019,2,14]]},"DOI":"10.1145\/3299771.3299798","type":"proceedings-article","created":{"date-parts":[[2019,2,8]],"date-time":"2019-02-08T13:27:45Z","timestamp":1549632465000},"page":"1-5","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Formalizing GPU Instruction Set Architecture in Coq"],"prefix":"10.1145","author":[{"given":"Nitin","family":"Bhatia","sequence":"first","affiliation":[{"name":"IIIT-Bangalore, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Meenakshi","family":"D'Souza","sequence":"additional","affiliation":[{"name":"IIIT-Bangalore, India"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sujit Kumar","family":"Chakrabarti","sequence":"additional","affiliation":[{"name":"IIIT-Bangalore, India"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2019,2,14]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Retrieved","author":"NVIDIA Corporation","year":"2018","unstructured":"NVIDIA Corporation. 2018. CUDA Parallel Computing. Retrieved December 13, 2018 from https:\/\/www.nvidia.in\/object\/cuda-parallel-computing-in.html"},{"key":"e_1_3_2_1_2_1","volume-title":"Retrieved","author":"NVIDIA Corporation","year":"2018","unstructured":"NVIDIA Corporation. 2018. Parallel Thread Execution ISA Version 6.3. Retrieved December 13, 2018 from https:\/\/docs.nvidia.com\/cuda\/parallel-thread-execution\/index.html"},{"key":"e_1_3_2_1_4_1","volume-title":"Retrieved","author":"Khronos Group","year":"2018","unstructured":"Khronos Group. 2018. The open standard for parallel programming of heterogeneous systems. Retrieved December 13, 2018 from https:\/\/www.khronos.org\/opencl\/"},{"key":"e_1_3_2_1_5_1","first-page":"20","article-title":"The OpenGL ES\u00ae Shading Language","volume":"3","author":"Khronos Group","year":"2018","unstructured":"Khronos Group. 2018. The OpenGL ES\u00ae Shading Language, Version 3.20.4. Retrieved December 13, 2018 from https:\/\/www.khronos.org\/registry\/OpenGL\/specs\/es\/3.2\/GLSL_ES_Specification_3.20.pdf","journal-title":"Version"},{"key":"e_1_3_2_1_6_1","volume-title":"Retrieved","author":"Khronos Group","year":"2018","unstructured":"Khronos Group. 2018. OpenGL ES\u00ae, Version 3.2. Retrieved December 13, 2018 from https:\/\/www.khronos.org\/registry\/OpenGL\/index_es.php"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2505879.2505897"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111042"},{"key":"e_1_3_2_1_9_1","volume-title":"Retrieved","author":"Pierce Benjamin C.","year":"2018","unstructured":"Benjamin C. Pierce. 2018. Software Foundations Volume 2. Retrieved December 13, 2018 from https:\/\/softwarefoundations.cis.upenn.edu\/plf-current\/index.html"},{"key":"e_1_3_2_1_10_1","volume-title":"Retrieved","author":"Development Team The Coq","year":"2018","unstructured":"The Coq Development Team. 2018. The Coq Proof Assistant. Retrieved December 13, 2018 from https:\/\/coq.inria.fr\/"},{"volume-title":"Dependable Software Engineering. Theories","author":"Wang Jiawei","key":"e_1_3_2_1_11_1","unstructured":"Jiawei Wang, Ming Fu, Lei Qiao, and Xinyu Feng. 2017. Formalizing SPARCv8 Instruction Set Architecture in Coq. In Dependable Software Engineering. Theories, Tools, and Applications, Kim Guldstrand Larsen, Oleg Sokolsky, and Ji Wang (Eds.). Springer International Publishing, Cham, 300--316."}],"event":{"name":"ISEC'19: 12th Innovations in Software Engineering Conference","sponsor":["iSOFT iSOFT","ACM Association for Computing Machinery","Microsoft Microsoft","ACM India ACM India"],"location":"Pune India","acronym":"ISEC'19"},"container-title":["Proceedings of the 12th Innovations in Software Engineering Conference (formerly known as India Software Engineering Conference)"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3299771.3299798","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3299771.3299798","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:26:13Z","timestamp":1750206373000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3299771.3299798"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,2,14]]},"references-count":10,"alternative-id":["10.1145\/3299771.3299798","10.1145\/3299771"],"URL":"https:\/\/doi.org\/10.1145\/3299771.3299798","relation":{},"subject":[],"published":{"date-parts":[[2019,2,14]]},"assertion":[{"value":"2019-02-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}