{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,30]],"date-time":"2025-09-30T00:18:00Z","timestamp":1759191480920,"version":"3.44.0"},"reference-count":24,"publisher":"IEEE","license":[{"start":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T00:00:00Z","timestamp":1751760000000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2025,7,6]],"date-time":"2025-07-06T00:00:00Z","timestamp":1751760000000},"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,7,6]]},"DOI":"10.1109\/isvlsi65124.2025.11130337","type":"proceedings-article","created":{"date-parts":[[2025,8,27]],"date-time":"2025-08-27T18:20:15Z","timestamp":1756318815000},"page":"1-6","source":"Crossref","is-referenced-by-count":0,"title":["HW\/SW Formal Co-Verification of Rust-based Designs Using Hardware Abstraction Model"],"prefix":"10.1109","author":[{"given":"Sascha","family":"Neske","sequence":"first","affiliation":[{"name":"Infineon Technologies AG"}]},{"given":"Bryan","family":"Olmos","sequence":"additional","affiliation":[{"name":"Infineon Technologies AG"}]},{"given":"Shuhang","family":"Zhang","sequence":"additional","affiliation":[{"name":"Infineon Technologies AG"}]},{"given":"Martin","family":"Kroening","sequence":"additional","affiliation":[{"name":"Rheinisch Westfaelische Technische Hochschule Aachen"}]},{"given":"Stefan","family":"Lankes","sequence":"additional","affiliation":[{"name":"Rheinisch Westfaelische Technische Hochschule Aachen"}]},{"given":"Wolfgang","family":"Kunz","sequence":"additional","affiliation":[{"name":"Universität Kaiserslautern-Landau,Rheinland-Pfälzische Technische"}]},{"given":"Djones","family":"Lettnin","sequence":"additional","affiliation":[{"name":"Infineon Technologies AG"}]}],"member":"263","reference":[{"year":"2025","key":"ref1","article-title":"Rust Programming Language"},{"key":"ref2","article-title":"Evaluation of Rust for Embedded Security Systems","author":"Manczak","year":"2023","journal-title":"Embedded World"},{"year":"2025","key":"ref3","article-title":"Rust Programming Language: Unsafe Rust"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386036"},{"key":"ref5","article-title":"Handbook of model checking","volume":"10","author":"Clarke","year":"2018"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1109\/ASPDAC.2003.1195033"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/vlsi-soc62099.2024.10767822"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1145\/3061639.3062253"},{"key":"ref9","article-title":"Hardware\/software co-verification using path-based symbolic execution","author":"Mukherjee","year":"2020","journal-title":"arXiv preprint arXiv:2001.01324"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-48989-6_33"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.359.16"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1016\/c2021-0-02714-0"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2008.923410"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44577-3_12"},{"year":"2025","key":"ref15","article-title":"Kani Rust Verifier: A Bit-Precise Model Checker for Rust"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/3658644.3690275"},{"article-title":"Syncrim: Hardware\/software co-design for the risc-v architecture using high-level simulation in rust","year":"2024","author":"Dzialo","key":"ref17"},{"article-title":"Improving on c with rust an analysis of rusts preventative abilities","year":"2020","author":"Kevin","key":"ref18"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.7717\/peerj-cs.406"},{"volume-title":"The ICARUS Verilog Compilation System: iVerilog","year":"2025","key":"ref20"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1142\/9789814261456_0001"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1145\/368996.369025"},{"article-title":"MetaRTL Implementation of Floating-Point Adder and Multiplier with Various Precision","year":"2024","author":"Schwarz","key":"ref23"},{"volume-title":"OpenTitan Root of Trust","year":"2024","key":"ref24"}],"event":{"name":"2025 IEEE Computer Society Annual Symposium on VLSI (ISVLSI)","start":{"date-parts":[[2025,7,6]]},"location":"Kalamata, Greece","end":{"date-parts":[[2025,7,9]]}},"container-title":["2025 IEEE Computer Society Annual Symposium on VLSI (ISVLSI)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx8\/11129697\/11130193\/11130337.pdf?arnumber=11130337","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T17:50:19Z","timestamp":1759168219000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/11130337\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,7,6]]},"references-count":24,"URL":"https:\/\/doi.org\/10.1109\/isvlsi65124.2025.11130337","relation":{},"subject":[],"published":{"date-parts":[[2025,7,6]]}}}