{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,24]],"date-time":"2025-08-24T01:28:05Z","timestamp":1755998885228,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":57,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,6,1]],"date-time":"2021-06-01T00:00:00Z","timestamp":1622505600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"NSF (National Science Foundation)","doi-asserted-by":"publisher","award":["CNS-1856636 AM04,DGE-1762114"],"award-info":[{"award-number":["CNS-1856636 AM04,DGE-1762114"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2021,6]]},"DOI":"10.1145\/3458336.3465277","type":"proceedings-article","created":{"date-parts":[[2021,6,4]],"date-time":"2021-06-04T02:03:56Z","timestamp":1622772236000},"page":"183-190","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["An incremental path towards a safer OS kernel"],"prefix":"10.1145","author":[{"given":"Jialin","family":"Li","sequence":"first","affiliation":[{"name":"University of Washington"}]},{"given":"Samantha","family":"Miller","sequence":"additional","affiliation":[{"name":"University of Washington"}]},{"given":"Danyang","family":"Zhuo","sequence":"additional","affiliation":[{"name":"Duke University"}]},{"given":"Ang","family":"Chen","sequence":"additional","affiliation":[{"name":"Rice University"}]},{"given":"Jon","family":"Howell","sequence":"additional","affiliation":[{"name":"VMware Research"}]},{"given":"Thomas","family":"Anderson","sequence":"additional","affiliation":[{"name":"University of Washington"}]}],"member":"320","published-online":{"date-parts":[[2021,6,3]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"Autotest - Fully automated testing under linux. https:\/\/autotest.github.io\/.  Autotest - Fully automated testing under linux. https:\/\/autotest.github.io\/."},{"key":"e_1_3_2_1_2_1","unstructured":"Coccinelle: A Program Matching and Transformation Tool for Systems Code. https:\/\/coccinelle.gitlabpages.inria.fr\/website\/.  Coccinelle: A Program Matching and Transformation Tool for Systems Code. https:\/\/coccinelle.gitlabpages.inria.fr\/website\/."},{"key":"e_1_3_2_1_3_1","unstructured":"CVE-2020-12351 kernel: net: bluetooth: type confusion while processing AMP packets. https:\/\/bugzilla.redhat.com\/show_bug.cgi?id=1886521.  CVE-2020-12351 kernel: net: bluetooth: type confusion while processing AMP packets. https:\/\/bugzilla.redhat.com\/show_bug.cgi?id=1886521."},{"key":"e_1_3_2_1_4_1","unstructured":"Kernel self-test. https:\/\/kselftest.wiki.kernel.org\/.  Kernel self-test. https:\/\/kselftest.wiki.kernel.org\/."},{"key":"e_1_3_2_1_5_1","unstructured":"KernelCI. https:\/\/kernelci.org\/.  KernelCI. https:\/\/kernelci.org\/."},{"key":"e_1_3_2_1_6_1","unstructured":"ktest. https:\/\/elinux.org\/Ktest.  ktest. https:\/\/elinux.org\/Ktest."},{"key":"e_1_3_2_1_7_1","unstructured":"LKFT - Linaro's Linux Kernel Functional Test framework. https:\/\/lkft.linaro.org\/.  LKFT - Linaro's Linux Kernel Functional Test framework. https:\/\/lkft.linaro.org\/."},{"key":"e_1_3_2_1_8_1","unstructured":"[PATCH 00\/13] [RFC] Rust support. https:\/\/lkml.org\/lkml\/2021\/4\/14\/1023.  [PATCH 00\/13] [RFC] Rust support. https:\/\/lkml.org\/lkml\/2021\/4\/14\/1023."},{"key":"e_1_3_2_1_9_1","unstructured":"Smatch: pluggable static analysis for C. https:\/\/lwn.net\/Articles\/691882\/.  Smatch: pluggable static analysis for C. https:\/\/lwn.net\/Articles\/691882\/."},{"key":"e_1_3_2_1_10_1","volume-title":"Summer USENIX","author":"Accetta Mike","year":"1986","unstructured":"Mike Accetta , Robert Baron , William Bolosky , David Golub , Richard Rashid , Avadis Tevanian , and Michael Young . Mach : A New Kernel Foundation For UNIX Development . In Summer USENIX , 1986 . Mike Accetta, Robert Baron, William Bolosky, David Golub, Richard Rashid, Avadis Tevanian, and Michael Young. Mach: A New Kernel Foundation For UNIX Development. In Summer USENIX, 1986."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629579"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/224057.224077"},{"key":"e_1_3_2_1_13_1","volume-title":"OSDI","author":"Boos Kevin","year":"2020","unstructured":"Kevin Boos , Namitha Liyanage , Ramla Ijaz , and Lin Zhong . Theseus : an Experiment in Operating System Structure and State Management . In OSDI , 2020 . Kevin Boos, Namitha Liyanage, Ramla Ijaz, and Lin Zhong. Theseus: an Experiment in Operating System Structure and State Management. In OSDI, 2020."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629581"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/3291168.3291191"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359632"},{"key":"e_1_3_2_1_17_1","volume-title":"CoqPL","author":"Chajed Tej","year":"2020","unstructured":"Tej Chajed , Joseph Tassarotti , M. Frans Kaashoek , and Nickolai Zeldovich . Verifying concurrent Go code in Coq with Goose . CoqPL , 2020 . Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai Zeldovich. Verifying concurrent Go code in Coq with Goose. CoqPL, 2020."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132776"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/502059.502042"},{"key":"e_1_3_2_1_21_1","volume-title":"INRIA","author":"Coq","year":"2016","unstructured":"Coq development team. The Coq Proof Assistant Reference Manual, Version 8.5pl2 . INRIA , July 2016 . http:\/\/coq.inria.fr\/distrib\/current\/refman\/. Coq development team. The Coq Proof Assistant Reference Manual, Version 8.5pl2. INRIA, July 2016. http:\/\/coq.inria.fr\/distrib\/current\/refman\/."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/3291168.3291176"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/224057.224076"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/1267308.1267314"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/350853.350863"},{"key":"e_1_3_2_1_26_1","unstructured":"Go is an open source programming language that makes it easy to build simple reliable and efficient software. https:\/\/golang.org\/.  Go is an open source programming language that makes it easy to build simple reliable and efficient software. https:\/\/golang.org\/."},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/3026877.3026928"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978405"},{"key":"e_1_3_2_1_29_1","volume-title":"OSDI","author":"Hance Travis","year":"2020","unstructured":"Travis Hance , Andrea Lattuada , Chris Hawblitzel , Jon Howell , Rob Johnson , and Bryan Parno . Storage Systems are Distributed Systems (So Verify Them That Way!) . In OSDI , 2020 . Travis Hance, Andrea Lattuada, Chris Hawblitzel, Jon Howell, Rob Johnson, and Bryan Parno. Storage Systems are Distributed Systems (So Verify Them That Way!). In OSDI, 2020."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/2685048.2685062"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1243418.1243424"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3302424.3303985"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132786"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341302.3342071"},{"key":"e_1_3_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/224057.224075"},{"key":"e_1_3_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385971"},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043568"},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359657"},{"key":"e_1_3_2_1_43_1","volume-title":"FAST","author":"Miller Samantha","year":"2021","unstructured":"Samantha Miller , Kaiyuan Zhang , Mengqi Chen , Ryan Jennings , Ang Chen , Danyang Zhuo , and Thomas Anderson . High Velocity Kernel File Systems with Bento . In FAST , 2021 . Samantha Miller, Kaiyuan Zhang, Mengqi Chen, Ryan Jennings, Ang Chen, Danyang Zhuo, and Thomas Anderson. High Velocity Kernel File Systems with Bento. In FAST, 2021."},{"key":"e_1_3_2_1_44_1","volume-title":"OSDI","author":"Narayanan Vikram","year":"2020","unstructured":"Vikram Narayanan , Tianjiao Huang , David Detweiler , Dan Appel , Zhaofeng Li , Gerd Zellweger , and Anton Burtsev. RedLeaf : Isolation and Communication in a Safe Operating System . In OSDI , 2020 . Vikram Narayanan, Tianjiao Huang, David Detweiler, Dan Appel, Zhaofeng Li, Gerd Zellweger, and Anton Burtsev. RedLeaf: Isolation and Communication in a Safe Operating System. In OSDI, 2020."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359641"},{"key":"e_1_3_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3132747.3132748"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/1961296.1950401"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/358818.358822"},{"key":"e_1_3_2_1_49_1","unstructured":"Rust: A language empowering everyone to build reliable and efficient software. https:\/\/www.rust-lang.org\/.  Rust: A language empowering everyone to build reliable and efficient software. https:\/\/www.rust-lang.org\/."},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/77648.77653"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.5555\/3026877.3026879"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3409003"},{"key":"e_1_3_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2666356.2594340"},{"key":"e_1_3_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/173668.168635"},{"key":"e_1_3_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737958"},{"key":"e_1_3_2_1_56_1","unstructured":"The Z3 Theorem Prover. https:\/\/github.com\/Z3Prover\/z3.  The Z3 Theorem Prover. https:\/\/github.com\/Z3Prover\/z3."},{"key":"e_1_3_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359644"}],"event":{"name":"HotOS '21: Workshop on Hot Topics in Operating Systems","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems"],"location":"Ann Arbor Michigan","acronym":"HotOS '21"},"container-title":["Proceedings of the Workshop on Hot Topics in Operating Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3458336.3465277","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3458336.3465277","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3458336.3465277","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T21:28:19Z","timestamp":1750195699000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3458336.3465277"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6]]},"references-count":57,"alternative-id":["10.1145\/3458336.3465277","10.1145\/3458336"],"URL":"https:\/\/doi.org\/10.1145\/3458336.3465277","relation":{},"subject":[],"published":{"date-parts":[[2021,6]]},"assertion":[{"value":"2021-06-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}