{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T07:03:27Z","timestamp":1782975807830,"version":"3.54.5"},"reference-count":52,"publisher":"IEEE","license":[{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T00:00:00Z","timestamp":1779062400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/100006919","name":"Massachusetts Institute of Technology","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100006919","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"NSF","doi-asserted-by":"publisher","award":["2422053"],"award-info":[{"award-number":["2422053"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000144","name":"CNS","doi-asserted-by":"publisher","award":["2046359"],"award-info":[{"award-number":["2046359"]}],"id":[{"id":"10.13039\/100000144","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000143","name":"CCF","doi-asserted-by":"publisher","award":["2422052"],"award-info":[{"award-number":["2422052"]}],"id":[{"id":"10.13039\/100000143","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100005362","name":"ACE","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100005362","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"DARPA","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026,5,18]]},"DOI":"10.1109\/sp63933.2026.00201","type":"proceedings-article","created":{"date-parts":[[2026,7,1]],"date-time":"2026-07-01T19:34:20Z","timestamp":1782934460000},"page":"3548-3566","source":"Crossref","is-referenced-by-count":0,"title":["INSIGHT: Automatic Generation of Explanations for Efficient Identification of Hardware Bugs and Underspecifications"],"prefix":"10.1109","author":[{"given":"Vincent Quentin","family":"Ulitzsch","sequence":"first","affiliation":[{"name":"MIT CSAIL"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Alessandro","family":"Bertani","sequence":"additional","affiliation":[{"name":"Politecnico di Milano, MIT CSAIL"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Peter W.","family":"Deutsch","sequence":"additional","affiliation":[{"name":"MIT CSAIL"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David Langus","family":"Rodriguez","sequence":"additional","affiliation":[{"name":"Cornell University,MIT Lincoln Laboratory"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kelly","family":"Xu","sequence":"additional","affiliation":[{"name":"MIT CSAIL"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Aarti","family":"Gupta","sequence":"additional","affiliation":[{"name":"Princeton University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Sharad","family":"Malik","sequence":"additional","affiliation":[{"name":"Princeton University"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mengjia","family":"Yan","sequence":"additional","affiliation":[{"name":"MIT CSAIL"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"263","reference":[{"key":"ref1","author":"Graham","year":"2023","journal-title":"RISC-V verification and implications of the 5: 1 ratio of DV to design engineers"},{"key":"ref2","author":"Ormandy","year":"2026\u2013","journal-title":"Zenbleed"},{"key":"ref3","first-page":"7179","article-title":"Downfall: Exploiting speculative data gathering","volume-title":"32nd USENIX Security Symposium (USENIX Security 23)","author":"Moghimi","year":"2023"},{"key":"ref4","author":"Ormandy","year":"2026\u2013","journal-title":"Reptar"},{"key":"ref5","first-page":"5341","article-title":"Cascade: CPU fuzzing via intricate program generation","volume-title":"33rd USENIX Security Symposium (USENIX Security 24)","author":"Solt","year":"2024"},{"key":"ref6","first-page":"3219","article-title":"TheHuzz: Instruction fuzzing of processors using Golden-Reference models for finding SoftwareExploitable vulnerabilities","volume-title":"31st USENIX Security Symposium (USENIX Security 22)","author":"Kande","year":"2022"},{"key":"ref7","article-title":"Encarsia: evaluating cpu fuzzers via automatic bug injection","volume-title":"Proceedings of the 34th USENIX Conference on Security Symposium, ser. SEC \u201925. USA: USENIX Association","author":"B\u00f6lcskei","year":"2025"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO56248.2022.00081"},{"key":"ref9","first-page":"42","article-title":"End-to-end verification of processors with ISA-Formal","volume-title":"International Conference on Computer Aided Verification. Springer","author":"Reid","year":"2016"},{"key":"ref10","article-title":"Comprehensive formal verification of observational correctness for the cheriot-ibex processor","author":"Ploix","year":"2025","journal-title":"arXiv preprint"},{"key":"ref11","author":"Lee","year":"2026\u2013","journal-title":"RISC-V Torture Test Generator"},{"key":"ref12","author":"Group","year":"2026\u2013","journal-title":"FORCE-RISCV"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/FDL50818.2020.9232941"},{"key":"ref14","first-page":"1307","article-title":"MorFuzz: Fuzzing processor via runtime instruction morphing enhanced synchronizable co-simulation","volume-title":"32nd USENIX Security Symposium (USENIX Security 23)","author":"Xu","year":"2023"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1049\/iet-cdt:20070016"},{"key":"ref16","article-title":"RISCover: Automatic discovery of userexploitable architectural security vulnerabilities in closed-source riscv cpus","author":"Thomas","year":"2025","journal-title":"ghostwriteattack.com"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO56248.2022.00080"},{"key":"ref18","article-title":"The RISC-V instruction set manual, volume i: Unprivileged ISA document, version 20190608-baseratified","author":"Waterman","year":"2019","journal-title":"RISC-V Foundation, Tech. Rep"},{"key":"ref19","first-page":"1787","article-title":"GenHuzz: An efficient generative hardware fuzzer","volume-title":"34th USENIX Security Symposium (USENIX Security 25)","author":"Wu","year":"2025"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1023\/A:1014170513439"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/3282444"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_5"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837664"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45251-6_29"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"ref26","article-title":"Gurobi Optimizer Reference Manual","year":"2025","journal-title":"Gurobi Optimization, LLC"},{"key":"ref27","year":"2024","journal-title":"IBM ILOG CPLEX Optimization Studio 22.1.2: CPLEX User\u2019s Manual"},{"key":"ref28","year":"2024","journal-title":"lp_solve Reference Guide, MIT Department of Mathematics"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-68279-0_8"},{"key":"ref30","author":"Research","year":"2021","journal-title":"Sodor core"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/3897.001.0001"},{"key":"ref32","volume-title":"VerilogCoder: Autonomous Verilog Coding Agents with Graph-based Planning and Abstract Syntax Tree (AST)-based Waveform Tracing Tool","author":"Ho","year":"2024"},{"key":"ref33","article-title":"Verilator and systemperl","volume-title":"North American SystemC Users\u2019 Group, Design Automation Conference","author":"Snyder","year":"2004"},{"key":"ref34","author":"Pinto.","year":"2026\u2013","journal-title":"Kronos core"},{"key":"ref35","first-page":"1","article-title":"SonicBOOM: The 3rd Generation Berkeley Out-of-Order Machine","volume-title":"Fourth Workshop on Computer Architecture Research with RISC-V","volume":"5","author":"Zhao","year":"2020"},{"key":"ref36","article-title":"Fix issue where instructions can read stale data from register file bypass","year":"2020","journal-title":"GitHub Pull Request \\#376"},{"key":"ref37","year":"2026\u2013","journal-title":"Jasper formal property verification app"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0243-x"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908099"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_14"},{"key":"ref41","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386027"},{"key":"ref42","doi-asserted-by":"publisher","DOI":"10.34727\/2020\/isbn.978-3-85448-042-6_23"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-39322-9_10"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32304-2_16"},{"key":"ref45","doi-asserted-by":"publisher","DOI":"10.1109\/SP54263.2024.00180"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1145\/3669940.3707263"},{"key":"ref47","article-title":"OASIS: ILP-Guided Synthesis of Loop Invariants","volume-title":"NeurIPS 2020 Workshop on Computer-Assisted Programming","author":"Bhatia","year":"2020"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00103"},{"key":"ref49","first-page":"1361","article-title":"HyPFuzz: Formal-Assisted processor fuzzing","volume-title":"32nd USENIX Security Symposium (USENIX Security 23)","author":"Chen","year":"2023"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.1109\/HOST55118.2023.10133714"},{"key":"ref51","year":"2026\u2013","journal-title":"Heartbleed bug"},{"key":"ref52","first-page":"385","article-title":"ROP is Still Dangerous: Breaking Modern Defenses","volume-title":"23rd USENIX Security Symposium (USENIX Security 14)","author":"Carlini","year":"2014"}],"event":{"name":"2026 IEEE Symposium on Security and Privacy (SP)","location":"San Francisco, CA, USA","start":{"date-parts":[[2026,5,18]]},"end":{"date-parts":[[2026,5,21]]}},"container-title":["2026 IEEE Symposium on Security and Privacy (SP)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/11573355\/11573356\/11573561.pdf?arnumber=11573561","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T05:36:22Z","timestamp":1782970582000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11573561\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,5,18]]},"references-count":52,"URL":"https:\/\/doi.org\/10.1109\/sp63933.2026.00201","relation":{},"subject":[],"published":{"date-parts":[[2026,5,18]]}}}