{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:21:53Z","timestamp":1778498513257,"version":"3.51.4"},"reference-count":30,"publisher":"IEEE","license":[{"start":{"date-parts":[[2023,4,5]],"date-time":"2023-04-05T00:00:00Z","timestamp":1680652800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2023,4,5]],"date-time":"2023-04-05T00:00:00Z","timestamp":1680652800000},"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":[[2023,4,5]]},"DOI":"10.1109\/isqed57927.2023.10129397","type":"proceedings-article","created":{"date-parts":[[2023,5,24]],"date-time":"2023-05-24T17:33:09Z","timestamp":1684949589000},"page":"1-7","source":"Crossref","is-referenced-by-count":6,"title":["Polynomial Formal Verification of a Processor: A RISC-V Case Study"],"prefix":"10.1109","author":[{"given":"Lennart","family":"Weingarten","sequence":"first","affiliation":[{"name":"University of Bremen,Institute of Computer Science,Bremen,Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alireza","family":"Mahzoon","sequence":"additional","affiliation":[{"name":"University of Bremen,Institute of Computer Science,Bremen,Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mehran","family":"Goli","sequence":"additional","affiliation":[{"name":"University of Bremen,Institute of Computer Science,Bremen,Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rolf","family":"Drechsler","sequence":"additional","affiliation":[{"name":"University of Bremen\/DFKI,Institute of Computer Science,Bremen,Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58179-0_44"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56496-9_17"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_19"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-002-0081-6"},{"key":"ref30","author":"somenzi","year":"2018","journal-title":"CUDD CU decision diagram package release 2 7 0"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/BF00243132"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1145\/3487212.3487333"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/MTV.2003.1250267"},{"key":"ref1","first-page":"282","article-title":"Formal verification of an ARM processor","author":"patankar","year":"1999","journal-title":"VLSI Design"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2005.37"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/2024724.2024843"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_20"},{"key":"ref18","first-page":"526","article-title":"Gap-free processor verification by s2qed and property generation","author":"devarajegowda","year":"2020","journal-title":"DATE"},{"key":"ref24","first-page":"457","article-title":"Polynomial formal verification of arithmetic circuits","author":"drechsler","year":"2021","journal-title":"ICCIDE"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373811"},{"key":"ref26","author":"waterman","year":"2019","journal-title":"The RISC-V Instruction Set Manual Volume II Privileged Architecture"},{"key":"ref25","author":"waterman","year":"2019","journal-title":"The RISC-V instruction set manual volume i Unprivileged ISA"},{"key":"ref20","first-page":"121","article-title":"Applying SMT in symbolic execution of microcode","author":"franz\u00e9n","year":"2010","journal-title":"FMCAD"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08970-6_1"},{"key":"ref21","first-page":"129","article-title":"Automated formal verification of processors based on architectural models","author":"k\u00fchne","year":"2010","journal-title":"FMCAD"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1109\/12.73590"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1145\/123186.123222"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898719789"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1109\/ISVLSI54635.2022.00029"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/DSD57027.2022.00107"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/DDECS52668.2021.9417052"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/3508352.3561104"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1145\/307988.307989"},{"key":"ref6","article-title":"Polynomial formal verification of floating point adders","author":"kleinekath\u00f6fer","year":"2023","journal-title":"DATE"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1109\/DDECS54261.2022.9770156"}],"event":{"name":"2023 24th International Symposium on Quality Electronic Design (ISQED)","location":"San Francisco, CA, USA","start":{"date-parts":[[2023,4,5]]},"end":{"date-parts":[[2023,4,7]]}},"container-title":["2023 24th International Symposium on Quality Electronic Design (ISQED)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/10129281\/10129282\/10129397.pdf?arnumber=10129397","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,19]],"date-time":"2023-06-19T17:44:47Z","timestamp":1687196687000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10129397\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,4,5]]},"references-count":30,"URL":"https:\/\/doi.org\/10.1109\/isqed57927.2023.10129397","relation":{},"subject":[],"published":{"date-parts":[[2023,4,5]]}}}