Hyperkernel: Push-button verification of an OS kernel

Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, Xi Wang
[doi] [Google Scholar] [DBLP] [Citeseer]

Proceedings of the 26th Symposium on Operating Systems Principles
ACM
Pages 252-269
2017
Topic(s): os tools verification
  • A secure and formally verified Linux KVM hypervisor [li:sandp:2021]
  • Scaling symbolic evaluation for automated verification of systems code with Serval [nelson:sosp:2019]