Hyperkernel explores a push-button approach to building provably correct OS kernels.
Hyperkernel: Push-Button Verification of an OS Kernel.
Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang.
In Proceedings of the 26th ACM Symposium on Operating Systems Principles (SOSP), Shanghai, China, October 2017.
Porting Hyperkernel to the ARM Architecture.
Technical Report UW-CSE-17-08-02, University of Washington, August 2017.
We will be giving a talk and demo of Hyperkernel at the 2017 New England Systems Verification Day.
We will be presenting a poster and giving a talk at SOSP 2017 in Shanghai.
We are in the process of cleaning up the code for a release by the end of 2017.
You can reach us at