{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,7]],"date-time":"2026-07-07T02:50:21Z","timestamp":1783392621581,"version":"3.54.6"},"publisher-location":"New York, NY, USA","reference-count":69,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,10,14]],"date-time":"2017-10-14T00:00:00Z","timestamp":1507939200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,10,14]]},"DOI":"10.1145\/3132747.3132748","type":"proceedings-article","created":{"date-parts":[[2017,10,12]],"date-time":"2017-10-12T12:51:09Z","timestamp":1507812669000},"page":"252-269","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":72,"title":["Hyperkernel"],"prefix":"10.1145","author":[{"given":"Luke","family":"Nelson","sequence":"first","affiliation":[{"name":"University of Washington"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Helgi","family":"Sigurbjarnarson","sequence":"additional","affiliation":[{"name":"University of Washington"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kaiyuan","family":"Zhang","sequence":"additional","affiliation":[{"name":"University of Washington"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Dylan","family":"Johnson","sequence":"additional","affiliation":[{"name":"University of Washington"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"James","family":"Bornholt","sequence":"additional","affiliation":[{"name":"University of Washington"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Emina","family":"Torlak","sequence":"additional","affiliation":[{"name":"University of Washington"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xi","family":"Wang","sequence":"additional","affiliation":[{"name":"University of Washington"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2017,10,14]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.5555\/2342821.2342856"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_48"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2872362.2872404"},{"key":"e_1_3_2_2_4_1","first-page":"28","article-title":"AMD64 Architecture Programmer's Manual Volume 2","volume":"3","author":"AMD.","year":"2017","unstructured":"AMD. 2017 . AMD64 Architecture Programmer's Manual Volume 2 : System Programming. Rev. 3 . 28 . AMD. 2017. AMD64 Architecture Programmer's Manual Volume 2: System Programming. Rev. 3.28.","journal-title":"System Programming. Rev."},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/106972.106984"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1108792.1108813"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629579"},{"key":"e_1_3_2_2_8_1","volume-title":"Proceedings of the 10th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Belay Adam","year":"2012","unstructured":"Adam Belay , Andrea Bittau , Ali Mashtizadeh , David Terei , David Mazi\u00e8res , and Christos Kozyrakis . 2012 . Dune: Safe User-level Access to Privileged CPU Features . In Proceedings of the 10th Symposium on Operating Systems Design and Implementation (OSDI) . Hollywood, CA, 335--348. Adam Belay, Andrea Bittau, Ali Mashtizadeh, David Terei, David Mazi\u00e8res, and Christos Kozyrakis. 2012. Dune: Safe User-level Access to Privileged CPU Features. In Proceedings of the 10th Symposium on Operating Systems Design and Implementation (OSDI). Hollywood, CA, 335--348."},{"key":"e_1_3_2_2_9_1","volume-title":"Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Belay Adam","year":"2014","unstructured":"Adam Belay , George Prekas , Ana Klimovic , Samuel Grossman , Christos Kozyrakis , and Edouard Bugnion . 2014 . IX: A Protected Dataplane Operating System for High Throughput and Low Latency . In Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI) . Broomfield, CO, 49--65. Adam Belay, George Prekas, Ana Klimovic, Samuel Grossman, Christos Kozyrakis, and Edouard Bugnion. 2014. IX: A Protected Dataplane Operating System for High Throughput and Low Latency. In Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI). Broomfield, CO, 49--65."},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.41331"},{"key":"e_1_3_2_2_11_1","volume-title":"Proceedings of the 8th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar , Daniel Dunbar , and Dawson Engler . 2008 . KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs . In Proceedings of the 8th Symposium on Operating Systems Design and Implementation (OSDI) . San Diego, CA, 209--224. Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proceedings of the 8th Symposium on Operating Systems Design and Implementation (OSDI). San Diego, CA, 209--224."},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103799.2103805"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815402"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/502034.502042"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522712"},{"issue":"6","key":"e_1_3_2_2_16_1","first-page":"1","article-title":"The Coq Proof Assistant Reference Manual","volume":"8","author":"Coq","year":"2017","unstructured":"Coq development team. 2017 . The Coq Proof Assistant Reference Manual , Version 8 . 6 . 1 . INRIA. http:\/\/coq.inria.fr\/distrib\/current\/refman\/. Coq development team. 2017. The Coq Proof Assistant Reference Manual, Version 8.6.1. INRIA. http:\/\/coq.inria.fr\/distrib\/current\/refman\/.","journal-title":"Version"},{"key":"e_1_3_2_2_17_1","volume-title":"Morris","author":"Cox Russ","year":"2016","unstructured":"Russ Cox , M. Frans Kaashoek , and Robert T . Morris . 2016 . Xv6, a simple Unix-like teaching operating system. http:\/\/pdos.csail.mit.edu\/6.828\/xv6. Russ Cox, M. Frans Kaashoek, and Robert T. Morris. 2016. Xv6, a simple Unix-like teaching operating system. http:\/\/pdos.csail.mit.edu\/6.828\/xv6."},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2541940.2541946"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_2_20_1","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner. 2011. Z3 - a Tutorial.  Leonardo de Moura and Nikolaj Bj\u00f8rner. 2011. Z3 - a Tutorial."},{"key":"e_1_3_2_2_21_1","volume-title":"Design and Implementation of the lwIP TCP\/IP Stack","author":"Dunkels Adam","unstructured":"Adam Dunkels . 2001. Design and Implementation of the lwIP TCP\/IP Stack . Swedish Institute of Computer Science . Adam Dunkels. 2001. Design and Implementation of the lwIP TCP\/IP Stack. Swedish Institute of Computer Science."},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522720"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/224056.224076"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/800214.806547"},{"key":"e_1_3_2_2_25_1","volume-title":"Proceedings of the 12th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu , Zhong Shao , Hao Chen , Xiongnan (Newman) Wu , Jieung Kim , Vilhelm Sj\u00f6berg , and David Costanzo . 2016 . CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels . In Proceedings of the 12th Symposium on Operating Systems Design and Implementation (OSDI) . Savannah, GA, 653--669. Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In Proceedings of the 12th Symposium on Operating Systems Design and Implementation (OSDI). Savannah, GA, 653--669."},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737979"},{"key":"e_1_3_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_2_28_1","volume-title":"Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Hawblitzel Chris","year":"2014","unstructured":"Chris Hawblitzel , Jon Howell , Jacob R. Lorch , Arjun Narayan , Bryan Parno , Danfeng Zhang , and Brian Zill . 2014 . Ironclad Apps: End-to-End Security via Automated Full-System Verification . In Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI) . Broomfield, CO, 165--181. Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. 2014. Ironclad Apps: End-to-End Security via Automated Full-System Verification. In Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI). Broomfield, CO, 165--181."},{"key":"e_1_3_2_2_29_1","unstructured":"Architecture Specification. Rev. 2016 2 4 Intel Virtualization Technology for Directed I\/O"},{"key":"e_1_3_2_2_30_1","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"Jackson Daniel","year":"2012","unstructured":"Daniel Jackson . 2012 . Software Abstractions: Logic, Language, and Analysis . MIT Press . Daniel Jackson. 2012. Software Abstractions: Logic, Language, and Analysis. MIT Press."},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158154"},{"key":"e_1_3_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/268998.266644"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560537"},{"key":"e_1_3_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_2_36_1","volume-title":"Design and Verification of Microprocessor Systems for High-Assurance Applications","author":"Klein Gerwin","unstructured":"Gerwin Klein , Thomas Sewell , and Simon Winwood . 2010. Refinement in the Formal Verification of the seL4 Microkernel . In Design and Verification of Microprocessor Systems for High-Assurance Applications . Springer , 323--339. Gerwin Klein, Thomas Sewell, and Simon Winwood. 2010. Refinement in the Formal Verification of the seL4 Microkernel. In Design and Verification of Microprocessor Systems for High-Assurance Applications. Springer, 323--339."},{"key":"e_1_3_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_20"},{"key":"e_1_3_2_2_40_1","volume-title":"Subtleties of the ANSI\/ISO C standard. Document N1639. ISO\/IEC JTC1\/SC22\/WG14","author":"Krebbers Robbert","unstructured":"Robbert Krebbers and Freek Wiedijk . 2012. Subtleties of the ANSI\/ISO C standard. Document N1639. ISO\/IEC JTC1\/SC22\/WG14 . Robbert Krebbers and Freek Wiedijk. 2012. Subtleties of the ANSI\/ISO C standard. Document N1639. ISO\/IEC JTC1\/SC22\/WG14."},{"key":"e_1_3_2_2_41_1","unstructured":"Chris Lattner. 2011. What Every C Programmer Should Know About Undefined Behavior. http:\/\/blog.llvm.org\/2011\/05\/what-every-c-programmer-should-know.html.  Chris Lattner. 2011. What Every C Programmer Should Know About Undefined Behavior. http:\/\/blog.llvm.org\/2011\/05\/what-every-c-programmer-should-know.html."},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.5555\/977395.977673"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062343"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/1939141.1939161"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2818302.2818306"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.1982.1653971"},{"key":"e_1_3_2_2_47_1","unstructured":"Linux Programmer's Manual 2016. dup dup2 dup3 - duplicate a file descriptor. http:\/\/man7.org\/linux\/man-pages\/man2\/dup.2.html.  Linux Programmer's Manual 2016. dup dup2 dup3 - duplicate a file descriptor. http:\/\/man7.org\/linux\/man-pages\/man2\/dup.2.html."},{"key":"e_1_3_2_2_48_1","volume-title":"Lions' Commentary on Unix","author":"Lions John","unstructured":"John Lions . 1996. Lions' Commentary on Unix ( 6 th ed.). Peer-to-Peer Communications . John Lions. 1996. Lions' Commentary on Unix (6th ed.). Peer-to-Peer Communications.","edition":"6"},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737965"},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560012"},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/2451116.2451148"},{"key":"e_1_3_2_2_52_1","first-page":"99","article-title":"System V Application Binary Interface: AMD64 Architecture Processor Supplement","volume":"0","author":"Matz Michael","year":"2014","unstructured":"Michael Matz , Jan Hubicka , Andreas Jaeger , and Mark Mitchell . 2014 . System V Application Binary Interface: AMD64 Architecture Processor Supplement , Draft Version 0 . 99 .7. Michael Matz, Jan Hubicka, Andreas Jaeger, and Mark Mitchell. 2014. System V Application Binary Interface: AMD64 Architecture Processor Supplement, Draft Version 0.99.7.","journal-title":"Draft Version"},{"key":"e_1_3_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2908080.2908081"},{"key":"e_1_3_2_2_54_1","volume-title":"A Proof Assistant for Higher-Order Logic","author":"Nipkow Tobias","unstructured":"Tobias Nipkow , Lawrence C. Paulson , and Markus Wenzel . 2016. Isabelle\/HOL : A Proof Assistant for Higher-Order Logic . Springer-Verlag . Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. 2016. Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer-Verlag."},{"key":"e_1_3_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1950365.1950401"},{"key":"e_1_3_2_2_56_1","volume-title":"Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Peter Simon","year":"2014","unstructured":"Simon Peter , Jialin Li , Irene Zhang , Dan R. K. Ports , Doug Woos , Arvind Krishnamurthy , Thomas Anderson , and Timothy Roscoe . 2014 . Arrakis: The Operating System is the Control Plane . In Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI) . Broomfield, CO, 1--16. Simon Peter, Jialin Li, Irene Zhang, Dan R. K. Ports, Doug Woos, Arvind Krishnamurthy, Thomas Anderson, and Timothy Roscoe. 2014. Arrakis: The Operating System is the Control Plane. In Proceedings of the 11th Symposium on Operating Systems Design and Implementation (OSDI). Broomfield, CO, 1--16."},{"key":"e_1_3_2_2_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462169"},{"key":"e_1_3_2_2_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_7"},{"key":"e_1_3_2_2_59_1","volume-title":"Patina: A Formalization of the Rust Programming Language. Technical Report UW-CSE-15-03-02","author":"Reed Eric","year":"2015","unstructured":"Eric Reed . 2015 . Patina: A Formalization of the Rust Programming Language. Technical Report UW-CSE-15-03-02 . University of Washington. Eric Reed. 2015. Patina: A Formalization of the Rust Programming Language. Technical Report UW-CSE-15-03-02. University of Washington."},{"key":"e_1_3_2_2_60_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133912"},{"key":"e_1_3_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594338"},{"key":"e_1_3_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43652-3_2"},{"key":"e_1_3_2_2_63_1","volume-title":"Proceedings of the 12th Symposium on Operating Systems Design and Implementation (OSDI)","author":"Sigurbjarnarson Helgi","year":"2016","unstructured":"Helgi Sigurbjarnarson , James Bornholt , Emina Torlak , and Xi Wang . 2016 . Push-Button Verification of File Systems via Crash Refinement . In Proceedings of the 12th Symposium on Operating Systems Design and Implementation (OSDI) . Savannah, GA, 1--16. Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. 2016. Push-Button Verification of File Systems via Crash Refinement. In Proceedings of the 12th Symposium on Operating Systems Design and Implementation (OSDI). Savannah, GA, 1--16."},{"key":"e_1_3_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1145\/195473.195515"},{"key":"e_1_3_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_3_2_2_66_1","doi-asserted-by":"publisher","DOI":"10.1145\/358818.358825"},{"key":"e_1_3_2_2_67_1","doi-asserted-by":"publisher","DOI":"10.1145\/2517349.2522728"},{"key":"e_1_3_2_2_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_4"},{"key":"e_1_3_2_2_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806610"},{"key":"e_1_3_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3098822.3098833"},{"key":"e_1_3_2_2_71_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375624"},{"key":"e_1_3_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103709"}],"event":{"name":"SOSP '17: ACM SIGOPS 26th Symposium on Operating Systems Principles","location":"Shanghai China","acronym":"SOSP '17","sponsor":["SIGOPS ACM Special Interest Group on Operating Systems","USENIX Assoc USENIX Assoc"]},"container-title":["Proceedings of the 26th Symposium on Operating Systems Principles"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3132747.3132748","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3132747.3132748","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:10:57Z","timestamp":1750212657000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3132747.3132748"}},"subtitle":["Push-Button Verification of an OS Kernel"],"short-title":[],"issued":{"date-parts":[[2017,10,14]]},"references-count":69,"alternative-id":["10.1145\/3132747.3132748","10.1145\/3132747"],"URL":"https:\/\/doi.org\/10.1145\/3132747.3132748","relation":{},"subject":[],"published":{"date-parts":[[2017,10,14]]},"assertion":[{"value":"2017-10-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}