{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,22]],"date-time":"2025-08-22T05:13:00Z","timestamp":1755839580612,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":17,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,8,24]],"date-time":"2023-08-24T00:00:00Z","timestamp":1692835200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"National Cyber Security Centre, UK"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,8,24]]},"DOI":"10.1145\/3609510.3609821","type":"proceedings-article","created":{"date-parts":[[2023,7,31]],"date-time":"2023-07-31T16:08:44Z","timestamp":1690819724000},"page":"9-15","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["First steps in verifying the seL4 Core Platform"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0009-8208-2946","authenticated-orcid":false,"given":"Mathieu","family":"Paturel","sequence":"first","affiliation":[{"name":"Trustworthy Systems Research Group, UNSW Sydney"}]},{"ORCID":"https:\/\/orcid.org\/0009-0001-2401-1682","authenticated-orcid":false,"given":"Isitha","family":"Subasinghe","sequence":"additional","affiliation":[{"name":"Trustworthy Systems Research Group, UNSW Sydney"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7069-0831","authenticated-orcid":false,"given":"Gernot","family":"Heiser","sequence":"additional","affiliation":[{"name":"Trustworthy Systems Research Group, UNSW Sydney"}]}],"member":"320","published-online":{"date-parts":[[2023,8,24]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Weakest-Precondition of Unstructured Programs. In ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE). Lisbon, PT.","author":"Barnett Mike","year":"2005","unstructured":"Mike Barnett and K. Rustan M. Leino . 2005 . Weakest-Precondition of Unstructured Programs. In ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE). Lisbon, PT. Mike Barnett and K. Rustan M. Leino. 2005. Weakest-Precondition of Unstructured Programs. In ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE). Lisbon, PT."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/365230.365252"},{"volume-title":"Can We Put the \"S\" Into IoT?","author":"Heiser Gernot","key":"e_1_3_2_1_3_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_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1851276.1851284"},{"key":"e_1_3_2_1_7_1","volume-title":"Light-Weight OS Mechanism for Managing Time. In EuroSys Conference. ACM","author":"Lyons Anna","year":"2018","unstructured":"Anna Lyons , Kent McLeod , Hesham Almatary , and Gernot Heiser . 2018 . Scheduling-Context Capabilities: A Principled , Light-Weight OS Mechanism for Managing Time. In EuroSys Conference. ACM , Porto, Portugal, 14. Anna Lyons, Kent McLeod, Hesham Almatary, and Gernot Heiser. 2018. Scheduling-Context Capabilities: A Principled, Light-Weight OS Mechanism for Managing Time. In EuroSys Conference. ACM, Porto, Portugal, 14."},{"key":"e_1_3_2_1_8_1","volume-title":"Sky-Bridge: Fast and Secure Inter-Process Communication for Microkernels. In EuroSys Conference. ACM","author":"Mi Zeyu","year":"2019","unstructured":"Zeyu Mi , Dingji Li , Zihan Yang , Xinran Wang , and Haibo Chen . 2019 . Sky-Bridge: Fast and Secure Inter-Process Communication for Microkernels. In EuroSys Conference. ACM , Dresden, DE, 15. Zeyu Mi, Dingji Li, Zihan Yang, Xinran Wang, and Haibo Chen. 2019. Sky-Bridge: Fast and Secure Inter-Process Communication for Microkernels. In EuroSys Conference. ACM, Dresden, DE, 15."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359641"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"volume-title":"OS Kernel. In ACM Symposium on Operating Systems Principles. ACM, 252--269","author":"Verification","key":"e_1_3_2_1_11_1","unstructured":"Verification of an OS Kernel. In ACM Symposium on Operating Systems Principles. ACM, 252--269 . Verification of an OS Kernel. In ACM Symposium on Operating Systems Principles. ACM, 252--269."},{"key":"e_1_3_2_1_12_1","unstructured":"Lucy Parker. 2022. The seL4 Device Driver Framework (sDDF). Talk at the seL4 Summit. https:\/\/sel4.systems\/Foundation\/Summit\/abstracts2022#a-sDDF  Lucy Parker. 2022. The seL4 Device Driver Framework (sDDF). Talk at the seL4 Summit. https:\/\/sel4.systems\/Foundation\/Summit\/abstracts2022#a-sDDF"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2797022.2797042"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462183"},{"key":"e_1_3_2_1_16_1","unstructured":"Nick Spinale. 2023. Rust-seL4 CapDL Loader. https:\/\/gitlab.com\/coliasgroup\/rust-seL4\/-\/tree\/main\/crates\/capdl  Nick Spinale. 2023. Rust-seL4 CapDL Loader. https:\/\/gitlab.com\/coliasgroup\/rust-seL4\/-\/tree\/main\/crates\/capdl"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951924"},{"key":"e_1_3_2_1_18_1","unstructured":"Trustworthy Systems. 2023. The seL4 Core Platform. https:\/\/trustworthy.systems\/projects\/TS\/sel4cp\/  Trustworthy Systems. 2023. The seL4 Core Platform. https:\/\/trustworthy.systems\/projects\/TS\/sel4cp\/"}],"event":{"name":"APSys '23: 14th ACM SIGOPS Asia-Pacific Workshop on Systems","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"],"location":"Seoul Republic of Korea","acronym":"APSys '23"},"container-title":["Proceedings of the 14th ACM SIGOPS Asia-Pacific Workshop on Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3609510.3609821","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3609510.3609821","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:46:25Z","timestamp":1750178785000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3609510.3609821"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,8,24]]},"references-count":17,"alternative-id":["10.1145\/3609510.3609821","10.1145\/3609510"],"URL":"https:\/\/doi.org\/10.1145\/3609510.3609821","relation":{},"subject":[],"published":{"date-parts":[[2023,8,24]]},"assertion":[{"value":"2023-08-24","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}