{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,13]],"date-time":"2025-11-13T17:23:41Z","timestamp":1763054621162,"version":"3.45.0"},"publisher-location":"New York, NY, USA","reference-count":19,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,10,13]]},"DOI":"10.1145\/3764860.3768335","type":"proceedings-article","created":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T13:54:43Z","timestamp":1759326883000},"page":"60-67","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["High-Fidelity Specification of Real-World Devices"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-3306-527X","authenticated-orcid":false,"given":"Liam","family":"Murphy","sequence":"first","affiliation":[{"name":"UNSW Sydney, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-9285-0980","authenticated-orcid":false,"given":"Albert","family":"Rizaldi","sequence":"additional","affiliation":[{"name":"PlanV GmbH, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-6234-3427","authenticated-orcid":false,"given":"Lesley","family":"Rossouw","sequence":"additional","affiliation":[{"name":"UNSW Sydney, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-4282-3923","authenticated-orcid":false,"given":"Chen","family":"George","sequence":"additional","affiliation":[{"name":"University of Wisconsin - Madison, U.S.A."}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-4712-5128","authenticated-orcid":false,"given":"James","family":"Treloar","sequence":"additional","affiliation":[{"name":"UNSW Sydney, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3488-7004","authenticated-orcid":false,"given":"Hammond","family":"Pearce","sequence":"additional","affiliation":[{"name":"UNSW Sydney, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-0739-1876","authenticated-orcid":false,"given":"Miki","family":"Tanaka","sequence":"additional","affiliation":[{"name":"UNSW Sydney, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7069-0831","authenticated-orcid":false,"given":"Gernot","family":"Heiser","sequence":"additional","affiliation":[{"name":"UNSW Sydney, Australia"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,10,13]]},"reference":[{"volume-title":"Verified Software: Theories, Tools and Experiments (Lecture Notes in Computer Science)","author":"Alkassar Eyad","key":"e_1_3_2_1_1_1","unstructured":"Eyad Alkassar, Mark Hillebrand, Dirk Leinenbach, Norbert Schirmer, and Artem Starostin. 2008. The Verisoft Approach to Systems Verification. In Verified Software: Theories, Tools and Experiments (Lecture Notes in Computer Science), Vol. 5295. Springer, 209--224."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3694715.3695956"},{"key":"e_1_3_2_1_3_1","volume-title":"Verifying Hardware Security Modules with Information-Preserving Refinement. In USENIX Symposium on Operating Systems Design and Implementation. 503--519","author":"Athalye Anish","year":"2022","unstructured":"Anish Athalye, M. Frans Kaashoek, and Nickolai Zeldovich. 2022. Verifying Hardware Security Modules with Information-Preserving Refinement. In USENIX Symposium on Operating Systems Design and Implementation. 503--519. https:\/\/www.usenix.org\/conference\/osdi22\/presentation\/athalye"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/83471.83475"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454065"},{"key":"e_1_3_2_1_6_1","unstructured":"Gernot Heiser Peter Chubb Alex Brown Julia Broady Courtney Darville and Lucy Parker. 2024. The seL4 Device Driver Framework (sDDF). https:\/\/trustworthy.systems\/projects\/drivers\/sddf-design.pdf"},{"key":"e_1_3_2_1_7_1","unstructured":"Andreas L\u00f6\u00f6w. 2018. Verilog development and verification project for HOL4. https:\/\/github.com\/CakeML\/hardware"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314622"},{"volume-title":"Proceedings of the International Workshop on Formal Methods in Software Engineering (FormaliSE@ICSE). 99--108","author":"L\u00f6\u00f6w Andreas","key":"e_1_3_2_1_9_1","unstructured":"Andreas L\u00f6\u00f6w and Magnus O. Myreen. 2019. A proof-producing translator for Verilog development in HOL. In Proceedings of the International Workshop on Formal Methods in Software Engineering (FormaliSE@ICSE). 99--108."},{"issue":"0","key":"e_1_3_2_1_10_1","article-title":"UM10204: I2C-bus specification and user manual","volume":"7","author":"NXP","year":"2021","unstructured":"NXP 2021. UM10204: I2C-bus specification and user manual, Rev. 7.0. https:\/\/www.nxp.com\/docs\/en\/user-guide\/UM10204.pdf","journal-title":"Rev."},{"key":"e_1_3_2_1_11_1","unstructured":"OpenTitan Developers. 2021. Selected peripherals from OpenTitan with PULP patches. https:\/\/github.com\/pulp-platform\/opentitan_peripherals"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCSII.2023.3289186"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3623759.3624544"},{"key":"e_1_3_2_1_14_1","unstructured":"PULP Developers. 2023. PULP Ethernet. https:\/\/github.com\/pulp-platform\/pulp-ethernet"},{"key":"e_1_3_2_1_15_1","volume-title":"Dingo: Taming Device Drivers. In EuroSys Conference","author":"Ryzhyk Leonid","year":"2009","unstructured":"Leonid Ryzhyk, Peter Chubb, Ihor Kuz, and Gernot Heiser. 2009a. Dingo: Taming Device Drivers. In EuroSys Conference. Nuremberg, DE, 275--288."},{"key":"e_1_3_2_1_16_1","volume-title":"Automatic Device Driver Synthesis with Termite. In ACM Symposium on Operating Systems Principles","author":"Ryzhyk Leonid","year":"2009","unstructured":"Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Etienne Le Sueur, and Gernot Heiser. 2009b. Automatic Device Driver Synthesis with Termite. In ACM Symposium on Operating Systems Principles. Big Sky, MT, US, 73--86."},{"key":"e_1_3_2_1_17_1","volume-title":"User-Guided Device Driver Synthesis. In USENIX Symposium on Operating Systems Design and Implementation","author":"Ryzhyk Leonid","year":"2014","unstructured":"Leonid Ryzhyk, Adam Christopher Walker, John Keys, Alexander Legg, Arun Raghunath, Michael Stumm, and Mona Vij. 2014. User-Guided Device Driver Synthesis. In USENIX Symposium on Operating Systems Design and Implementation. Broomfield, CO, USA, 661--676."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_6"},{"key":"e_1_3_2_1_19_1","unstructured":"Yosys Developers. 2020. Equivalence checking with Yosys. https:\/\/github.com\/YosysHQ\/eqy"}],"event":{"name":"SOSP '25: ACM SIGOPS 31st Symposium on Operating Systems Principles","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"],"location":"Seoul Republic of Korea","acronym":"SOSP '25"},"container-title":["Proceedings of the 13th Workshop on Programming Languages and Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3764860.3768335","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,13]],"date-time":"2025-11-13T17:20:27Z","timestamp":1763054427000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3764860.3768335"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,13]]},"references-count":19,"alternative-id":["10.1145\/3764860.3768335","10.1145\/3764860"],"URL":"https:\/\/doi.org\/10.1145\/3764860.3768335","relation":{},"subject":[],"published":{"date-parts":[[2025,10,13]]},"assertion":[{"value":"2025-10-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}