{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T05:56:47Z","timestamp":1763704607231,"version":"3.45.0"},"reference-count":53,"publisher":"IEEE","license":[{"start":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T00:00:00Z","timestamp":1761436800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2025,10,26]],"date-time":"2025-10-26T00:00:00Z","timestamp":1761436800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"DOI":"10.13039\/501100002367","name":"Chinese Academy of Sciences","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100002367","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,10,26]]},"DOI":"10.1109\/iccad66269.2025.11240887","type":"proceedings-article","created":{"date-parts":[[2025,11,20]],"date-time":"2025-11-20T18:39:34Z","timestamp":1763663974000},"page":"1-9","source":"Crossref","is-referenced-by-count":0,"title":["BMCFuzz: Hybrid Verification of Processors by Synergistic Integration of Bound Model Checking and Fuzzing"],"prefix":"10.1109","author":[{"given":"Shidong","family":"Shen","sequence":"first","affiliation":[{"name":"Institute of Software, Chinese Academy of Sciences,Key Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science,Beijing,China"}]},{"given":"Jinyu","family":"Liu","sequence":"additional","affiliation":[{"name":"Institute of Software, Chinese Academy of Sciences,Key Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science,Beijing,China"}]},{"given":"Weizhi","family":"Feng","sequence":"additional","affiliation":[{"name":"Institute of Software, Chinese Academy of Sciences,Key Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science,Beijing,China"}]},{"given":"Fu","family":"Song","sequence":"additional","affiliation":[{"name":"Institute of Software, Chinese Academy of Sciences,Key Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science,Beijing,China"}]},{"given":"Zhilin","family":"Wu","sequence":"additional","affiliation":[{"name":"Institute of Software, Chinese Academy of Sciences,Key Laboratory of System Software (Chinese Academy of Sciences) and State Key Laboratory of Computer Science,Beijing,China"}]}],"member":"263","reference":[{"article-title":"The emergence of hardware fuzzing: A critical review of its significance","year":"2024","author":"Saravanan","key":"ref1"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-59047-1_50"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-5693-0"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1007\/978-981-96-0602-3_8"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8"},{"issue":"3","key":"ref6","first-page":"13","article-title":"Constraint-based random stimuli generation for hardware verification","volume":"28","author":"Naveh","year":"2007","journal-title":"AI magazine"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.23919\/DATE56975.2023.10137202"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2020.2997644"},{"key":"ref9","first-page":"1361","article-title":"HyPFuzz: Formal-Assisted processor fuzzing","author":"Chen","year":"2023","journal-title":"USENIX Security"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1109\/ASP-DAC58780.2024.10473911"},{"year":"2019","key":"ref11","article-title":"Nutshell RISC-V CPU"},{"year":"2023","key":"ref12","article-title":"Rocket chip RISC-V CPU generator"},{"year":"2023","key":"ref13","article-title":"RISC-V Boom: The Berkeley out-of-order RISC-V processor"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1145\/2228360.2228584"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1109\/HOST55118.2023.10133714"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.21236\/ada605735"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1007\/s11390-023-3285-8"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1145\/3240765.3240842"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1145\/3582016.3582019"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/3649329.3655911"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1145\/3548606.3560602"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO56248.2022.00080"},{"article-title":"Verilator and systemperl","volume-title":"North American SystemC Users\u2019 Group, Design Automation Conference","author":"Snyder","key":"ref23"},{"year":"2023","key":"ref24","article-title":"Spike, a RISC-V isa simulator"},{"year":"2019","key":"ref25","article-title":"Difftest: a modern co-simulation framework for risc-v processors"},{"article-title":"Tutorial on world-level model checking","volume-title":"FMCAD","author":"Biere","key":"ref26"},{"article-title":"Symbiyosys","year":"2022","author":"Wolf","key":"ref27"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1145\/3649329.3655970"},{"year":"2024","key":"ref29","article-title":"Hardware Model Checking Competition 2024"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37703-7_1"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65627-9_7"},{"year":"2018","key":"ref32","article-title":"Random instruction generator for RISC-V processor verification"},{"year":"2015","key":"ref33","article-title":"riscv-tests"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/SP40001.2021.00103"},{"key":"ref35","first-page":"3219","article-title":"Thehuzz: Instruction fuzzing of processors using golden-reference models for finding software-exploitable vulnerabilities","author":"Kande","year":"2022","journal-title":"USENIX Security"},{"key":"ref36","doi-asserted-by":"publisher","DOI":"10.1109\/ICASSP49660.2025.10889404"},{"key":"ref37","first-page":"5341","article-title":"Cascade: CPU fuzzing via intricate program generation","author":"Solt","year":"2024","journal-title":"USENIX Security"},{"key":"ref38","doi-asserted-by":"publisher","DOI":"10.23919\/DATE58400.2024.10546625"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1145\/3526241.3530340"},{"key":"ref40","first-page":"1307","article-title":"MorFuzz: Fuzzing processor via runtime instruction morphing enhanced synchronizable co-simulation","author":"Xu","year":"2023","journal-title":"USENIX Security"},{"key":"ref41","first-page":"3237","article-title":"Fuzzing hardware like software","author":"Trippel","year":"2022","journal-title":"USENIX Security"},{"year":"2023","key":"ref42","article-title":"Questa Verification Environment"},{"year":"2023","key":"ref43","article-title":"VC Formal"},{"year":"2023","key":"ref44","article-title":"Jasper RTL Apps"},{"year":"2020","key":"ref45","article-title":"OneSpin 360 DV RISC-V Verification App"},{"year":"2023","key":"ref46","article-title":"FormalISA: RISC-V formal verification"},{"year":"2016","key":"ref47","article-title":"RISC-V Formal Verification Framework"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1109\/DAC18072.2020.9218572"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1109\/VLSID.2016.143"},{"key":"ref50","doi-asserted-by":"publisher","DOI":"10.23919\/DATE54114.2022.9774672"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1145\/2966986.2967079"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1023\/A:1011189608077"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.23919\/DATE.2018.8342260"}],"event":{"name":"2025 IEEE\/ACM International Conference On Computer Aided Design (ICCAD)","start":{"date-parts":[[2025,10,26]]},"location":"Munich, Germany","end":{"date-parts":[[2025,10,30]]}},"container-title":["2025 IEEE\/ACM International Conference On Computer Aided Design (ICCAD)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/11240608\/11240621\/11240887.pdf?arnumber=11240887","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,21]],"date-time":"2025-11-21T05:45:51Z","timestamp":1763703951000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11240887\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,26]]},"references-count":53,"URL":"https:\/\/doi.org\/10.1109\/iccad66269.2025.11240887","relation":{},"subject":[],"published":{"date-parts":[[2025,10,26]]}}}