Verifying the Microsoft Hyper-V Hypervisor with VCC

Dirk Leinenbach, Thomas Santen

In: 16th International Symposium on Formal Methods. International Symposium on Formal Methods (FM-2009) November 2-6 Eindhoven Netherlands Seiten 806-809 Lecture Notes in Computer Science 5850 Springer 2009.


VCC is an industrial-strength verification suite for the formal verification of concurrent, low-level C code. It is being developed by Microsoft Research, Redmond, and the European Microsoft Innovation Center, Aachen. The development is driven by two applications from the Verisoft~XT project: the Microsoft Hyper-V Hypervisor and SYSGO's PikeOS micro kernel. This paper gives a brief overview on the Hypervisor with a special focus on verification related challenges this kind of low-level software poses. It discusses how the design of VCC addresses these challenges, and highlights some specific issues of the Hypervisor verification and how they can be solved with VCC.


Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence