NOVA hypervisor

[Google Scholar] [Website]

Notes: Coq theorem prover, operating systems
Papers: becker:fm:2016

NOVA is a hypervisor (or micro-hypervisor) descended from L4.

todo:

  • Combining mechanized proofs and model-based testing in the formal analysis of a hypervisor [becker:fm:2016]