{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,2]],"date-time":"2026-07-02T00:54:23Z","timestamp":1782953663716,"version":"3.54.5"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,10,23]],"date-time":"2023-10-23T00:00:00Z","timestamp":1698019200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100006374","name":"Knut och Alice Wallenbergs Stiftelse","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100006374","id-type":"DOI","asserted-by":"publisher"}]},{"name":"National Cyber Security Centre"},{"name":"Technology Innovation Institute"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,10,23]]},"DOI":"10.1145\/3623759.3624544","type":"proceedings-article","created":{"date-parts":[[2023,10,14]],"date-time":"2023-10-14T13:05:51Z","timestamp":1697288751000},"page":"1-9","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Pancake"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6406-7875","authenticated-orcid":false,"given":"Johannes \u00c5man","family":"Pohjola","sequence":"first","affiliation":[{"name":"UNSW Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4923-3783","authenticated-orcid":false,"given":"Hira Taqdees","family":"Syeda","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Gothenburg, Sweden and Amazon Web Services"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-0739-1876","authenticated-orcid":false,"given":"Miki","family":"Tanaka","sequence":"additional","affiliation":[{"name":"UNSW Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-4232-1519","authenticated-orcid":false,"given":"Krishnan","family":"Winter","sequence":"additional","affiliation":[{"name":"UNSW Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-4132-0018","authenticated-orcid":false,"given":"Tsun Wang","family":"Sau","sequence":"additional","affiliation":[{"name":"UNSW Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-2789-0763","authenticated-orcid":false,"given":"Benjamin","family":"Nott","sequence":"additional","affiliation":[{"name":"UNSW Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1999-9219","authenticated-orcid":false,"given":"Tiana Tsang","family":"Ung","sequence":"additional","affiliation":[{"name":"UNSW Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1323-8566","authenticated-orcid":false,"given":"Craig","family":"McLaughlin","sequence":"additional","affiliation":[{"name":"UNSW Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-6226-1413","authenticated-orcid":false,"given":"Remy","family":"Seassau","sequence":"additional","affiliation":[{"name":"UNSW Sydney, Australia and University of Oxford"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9504-4107","authenticated-orcid":false,"given":"Magnus O.","family":"Myreen","sequence":"additional","affiliation":[{"name":"Chalmers University of Technology, Gothenburg, Sweden"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1163-8467","authenticated-orcid":false,"given":"Michael","family":"Norrish","sequence":"additional","affiliation":[{"name":"Australian National University, Canberra, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7069-0831","authenticated-orcid":false,"given":"Gernot","family":"Heiser","sequence":"additional","affiliation":[{"name":"UNSW Sydney, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,10,23]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"International Verification Workshop","author":"Alkassar E.","unstructured":"E. Alkassar, M. Hillebrand, S. Knapp, R. Rusev, and S. Tverdyshev. 2007. Formal Device and Programming Model for a Serial Interface. In International Verification Workshop. Bremen, DE, 4--20."},{"key":"e_1_3_2_1_2_1","volume-title":"Hillebrand","author":"Alkassar Eyad","year":"2008","unstructured":"Eyad Alkassar and Mark A. Hillebrand. 2008. Formal Functional Verification of Device Drivers. In Verified Software: Theories, Tools and Experiments (Lecture Notes in Computer Science, Vol. 5295). Springer, Toronto, Canada, 225--239."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872404"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-19718-5_1"},{"key":"e_1_3_2_1_5_1","volume-title":"Program Logics for Certified Compilers","author":"Appel Andrew W.","unstructured":"Andrew W. Appel, Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. 2014. Program Logics for Certified Compilers. Cambridge University Press, USA."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428204"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908101"},{"key":"e_1_3_2_1_8_1","volume-title":"Systems Software Verification","author":"Duan Jianjun","unstructured":"Jianjun Duan and John Regehr. 2010. Correctness Proofs for Device Drivers in Embedded Systems. In Systems Software Verification. USENIX Association, Vancouver, BC, CA."},{"key":"e_1_3_2_1_9_1","volume-title":"Technical Report T2001-20","author":"Dunkels Adam","year":"2001","unstructured":"Adam Dunkels. 2001. Minimal TCP\/IP implementation with proxy support. Technical Report T2001-20. SICS. 81 pages. http:\/\/www.sics.se\/~adam\/thesis.pdf."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377811.3380413"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428272"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594296"},{"key":"e_1_3_2_1_13_1","volume-title":"Can We Put the \"S\" Into IoT?","author":"Heiser Gernot","unstructured":"Gernot Heiser, Lucy Parker, Peter Chubb, Ivan Velickovic, and Ben Leslie. 2022. Can We Put the \"S\" Into IoT?. In IEEE World Forum on Internet of Things. Yokohama, JP."},{"key":"e_1_3_2_1_14_1","volume-title":"Proceedings of the General Track: 2002 USENIX Annual Technical Conference, June 10--15","author":"Jim Trevor","year":"2002","unstructured":"Trevor Jim, J. Gregory Morrisett, Dan Grossman, Michael W. Hicks, James Cheney, and Yanling Wang. 2002. Cyclone: A Safe Dialect of C. In Proceedings of the General Track: 2002 USENIX Annual Technical Conference, June 10--15, 2002, Monterey, California, USA. USENIX, 275--288. http:\/\/www.usenix.org\/publications\/library\/proceedings\/usenix02\/jim.html"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_2_1_16_1","volume-title":"K-Rust: An Executable Formal Semantics for Rust. CoRR abs\/1804.07608","author":"Kan Shuanglong","year":"2018","unstructured":"Shuanglong Kan, David San\u00e1n, Shang-Wei Lin, and Yang Liu. 2018. K-Rust: An Executable Formal Semantics for Rust. CoRR abs\/1804.07608 (2018). http:\/\/arxiv.org\/abs\/1804.07608 Preprint."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85114-1_12"},{"key":"e_1_3_2_1_18_1","unstructured":"Steve Klabnik and Carol Nichols. 2017. The Rust Programming Language. No Starch Press."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_1_22_1","unstructured":"MITRE Corporation. 2023. Linux >> Linux Kernel: Security Vulnerabilities (CVSS score \u2265 9). https:\/\/www.cvedetails.com\/vulnerability-list.php?vendor_id=33&product_id=47&version_id=&page=1&hasexp=0&opdos=0&opec=0&opov=0&opcsrf=0&opgpriv=0&opsqli=0&opxss=0&opdirt=0&opmemc=0&ophttprs=0&opbyp=0&opfileinc=0&opginf=0&cvssscoremin=9&cvssscoremax=0&year=0&month=0&cweid=0&order=1&trc=3034&sha=544260ec3a86a7e17f8b02b39d6342815d8d4bd5 Accessed: 2023-01-25."},{"key":"e_1_3_2_1_23_1","unstructured":"Tomas M\u00f6re. 2021. Formal verification of device driver monitors in HOL 4. Masters Thesis. School of EECS KTH SE."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","unstructured":"Magnus O. Myreen. 2021. A Minimalistic Verified Bootstrapped Compiler (Proof Pearl). In Certified Programs and Proofs (CPP). ACM 32--45. https:\/\/doi.org\/10.1145\/3437992.3439915","DOI":"10.1145\/3437992.3439915"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2008.ECP.24"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006277616879"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_23"},{"key":"e_1_3_2_1_28_1","volume-title":"The seL4 Device Driver Framework. https:\/\/trustworthy.systems\/publications\/papers\/Parker_23%3Asel4s.abstract Talk at the 5th seL4 Summit","author":"Parker Lucy","unstructured":"Lucy Parker. 2023. The seL4 Device Driver Framework. https:\/\/trustworthy.systems\/publications\/papers\/Parker_23%3Asel4s.abstract Talk at the 5th seL4 Summit."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_21"},{"key":"e_1_3_2_1_30_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. 2009. Dingo: Taming Device Drivers. In EuroSys Conference. Nuremberg, DE, 275--288."},{"key":"e_1_3_2_1_31_1","volume-title":"The Case for Active Device Drivers. In Asia-Pacific Workshop on Systems (APSys)","author":"Ryzhyk Leonid","year":"2010","unstructured":"Leonid Ryzhyk, Yanjin Zhu, and Gernot Heiser. 2010. The Case for Active Device Drivers. In Asia-Pacific Workshop on Systems (APSys). New Delhi, India, 25--30."},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462183"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71067-7_6"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000229"},{"key":"e_1_3_2_1_35_1","unstructured":"Trustworthy Systems. 2023. The seL4 Microkit. UNSW Sydney. https:\/\/trustworthy.systems\/projects\/microkit\/"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2018.00014"},{"key":"e_1_3_2_1_37_1","volume-title":"Oxide: The Essence of Rust. CoRR abs\/1903.00982","author":"Weiss Aaron","year":"2019","unstructured":"Aaron Weiss, Daniel Patterson, Nicholas D. Matsakis, and Amal Ahmed. 2019. Oxide: The Essence of Rust. CoRR abs\/1903.00982 (2019). http:\/\/arxiv.org\/abs\/1903.00982 Preprint."},{"key":"e_1_3_2_1_38_1","volume-title":"Conference for Unix, Linux and Open Source Professionals (AUUG)","author":"Wienand Ian","year":"2004","unstructured":"Ian Wienand and Luke Macpherson. 2004. ipbench: A Framework for Distributed Network Benchmarking. In Conference for Unix, Linux and Open Source Professionals (AUUG). Melbourne, Australia, 163--170."},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371119"}],"event":{"name":"SOSP '23: ACM SIGOPS 29th Symposium on Operating Systems Principles","location":"Koblenz Germany","acronym":"SOSP '23","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"]},"container-title":["Proceedings of the 12th Workshop on Programming Languages and Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3623759.3624544","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3623759.3624544","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,23]],"date-time":"2025-08-23T18:28:41Z","timestamp":1755973721000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3623759.3624544"}},"subtitle":["Verified Systems Programming Made Sweeter"],"short-title":[],"issued":{"date-parts":[[2023,10,23]]},"references-count":39,"alternative-id":["10.1145\/3623759.3624544","10.1145\/3623759"],"URL":"https:\/\/doi.org\/10.1145\/3623759.3624544","relation":{},"subject":[],"published":{"date-parts":[[2023,10,23]]},"assertion":[{"value":"2023-10-23","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}