{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T04:08:27Z","timestamp":1748750907739,"version":"3.41.0"},"reference-count":16,"publisher":"IEEE","license":[{"start":{"date-parts":[[2025,4,23]],"date-time":"2025-04-23T00:00:00Z","timestamp":1745366400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2025,4,23]],"date-time":"2025-04-23T00:00:00Z","timestamp":1745366400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,4,23]]},"DOI":"10.1109\/isqed65160.2025.11014422","type":"proceedings-article","created":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T17:43:30Z","timestamp":1748627010000},"page":"1-7","source":"Crossref","is-referenced-by-count":0,"title":["Formal Verification of a Custom Compiler for a Fully Homomorphic Encryption Accelerator"],"prefix":"10.1109","author":[{"given":"Zhenkun","family":"Yang","sequence":"first","affiliation":[{"name":"Intel Corporation,Intel Labs"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Suvadeep","family":"Banerjee","sequence":"additional","affiliation":[{"name":"Intel Corporation,Intel Labs"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeremy","family":"Casas","sequence":"additional","affiliation":[{"name":"Intel Corporation,Intel Labs"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jin","family":"Yang","sequence":"additional","affiliation":[{"name":"Intel Corporation,Intel Labs"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref1","article-title":"CertiCoq: A verified compiler for Coq","volume-title":"The third international workshop on Coq for programming languages (CoqPL)","author":"Anand","year":"2017"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/3560810.3565290"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1109\/DAC56929.2023.10247836"},{"volume-title":"DARPA Selects Researchers to Accelerate Use of Fully Homomorphic Encryption","year":"2021","key":"ref4"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/tec.1959.5219515"},{"key":"ref6","article-title":"A fully homomorphic encryption scheme","volume-title":"Stanford university","author":"Gentry","year":"2009"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/3591259"},{"key":"ref8","first-page":"163","article-title":"Closing the gap - The formally verified optimizing compiler CompCert","volume-title":"Developments in System Safety Engineering: Proc. of the 25th Safety-critical Systems Symposium","author":"K\u00e4stner","year":"2017"},{"key":"ref9","article-title":"Towards a Polynomial Instruction Based Compiler for Fully Homomorphic Encryption Ac-celerators","volume-title":"Cryptology ePrint Archive, Paper 2024\/707","author":"Kim","year":"2024"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1979.1675439"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/349299.349314"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/SP46214.2022.9833782"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054170"},{"key":"ref16","first-page":"4715","article-title":"HECO: Fully Homomorphic Encryption Compiler","volume-title":"32nd USENIX Security Symposium","author":"Viand"}],"event":{"name":"2025 26th International Symposium on Quality Electronic Design (ISQED)","start":{"date-parts":[[2025,4,23]]},"location":"San Francisco, CA, USA","end":{"date-parts":[[2025,4,25]]}},"container-title":["2025 26th International Symposium on Quality Electronic Design (ISQED)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/11014297\/11014302\/11014422.pdf?arnumber=11014422","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T05:00:47Z","timestamp":1748667647000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11014422\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,23]]},"references-count":16,"URL":"https:\/\/doi.org\/10.1109\/isqed65160.2025.11014422","relation":{},"subject":[],"published":{"date-parts":[[2025,4,23]]}}}