{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,4]],"date-time":"2025-05-04T02:08:07Z","timestamp":1746324487632,"version":"3.37.3"},"publisher-location":"New York, NY, USA","reference-count":39,"publisher":"ACM","funder":[{"DOI":"10.13039\/https:\/\/doi.org\/10.13039\/501100004063","name":"Knut och Alice Wallenbergs Stiftelse","doi-asserted-by":"publisher","id":[{"id":"10.13039\/https:\/\/doi.org\/10.13039\/501100004063","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-14T17:05:51Z","timestamp":1697303151000},"page":"1-9","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"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"}]},{"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"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-0739-1876","authenticated-orcid":false,"given":"Miki","family":"Tanaka","sequence":"additional","affiliation":[{"name":"UNSW Sydney, Australia"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-4232-1519","authenticated-orcid":false,"given":"Krishnan","family":"Winter","sequence":"additional","affiliation":[{"name":"UNSW Sydney, Australia"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-4132-0018","authenticated-orcid":false,"given":"Tsun Wang","family":"Sau","sequence":"additional","affiliation":[{"name":"UNSW Sydney, Australia"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-2789-0763","authenticated-orcid":false,"given":"Benjamin","family":"Nott","sequence":"additional","affiliation":[{"name":"UNSW Sydney, Australia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1999-9219","authenticated-orcid":false,"given":"Tiana Tsang","family":"Ung","sequence":"additional","affiliation":[{"name":"UNSW Sydney, Australia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1323-8566","authenticated-orcid":false,"given":"Craig","family":"McLaughlin","sequence":"additional","affiliation":[{"name":"UNSW Sydney, Australia"}]},{"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"}]},{"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"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1163-8467","authenticated-orcid":false,"given":"Michael","family":"Norrish","sequence":"additional","affiliation":[{"name":"Australian National University, Canberra, Australia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7069-0831","authenticated-orcid":false,"given":"Gernot","family":"Heiser","sequence":"additional","affiliation":[{"name":"UNSW Sydney, Australia"}]}],"member":"320","published-online":{"date-parts":[[2023,10,23]]},"reference":[{"volume-title":"International Verification Workshop","author":"Alkassar E.","key":"e_1_3_2_1_1_1","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. 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 . 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"},{"volume-title":"Program Logics for Certified Compilers","author":"Appel Andrew W.","key":"e_1_3_2_1_5_1","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. 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"},{"volume-title":"Systems Software Verification","author":"Duan Jianjun","key":"e_1_3_2_1_8_1","unstructured":"Jianjun Duan and John Regehr . 2010. Correctness Proofs for Device Drivers in Embedded Systems . In Systems Software Verification . USENIX Association , Vancouver, BC , CA. 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. 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"},{"volume-title":"Can We Put the \"S\" Into IoT?","author":"Heiser Gernot","key":"e_1_3_2_1_13_1","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. 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 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 . 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. 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. 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. 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","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"},{"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","key":"e_1_3_2_1_28_1","unstructured":"Lucy Parker . 2023. The seL4 Device Driver Framework. https:\/\/trustworthy.systems\/publications\/papers\/Parker_23%3Asel4s.abstract Talk at the 5th seL4 Summit . 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. 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. 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\/ 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 . 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. 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","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"],"location":"Koblenz Germany","acronym":"SOSP '23"},"container-title":["Proceedings of the 12th Workshop on Programming Languages and Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3623759.3624544","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,30]],"date-time":"2023-11-30T11:34:40Z","timestamp":1701344080000},"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":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}