Publikation
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, Pages 806-809, Lecture Notes in Computer Science, Vol. 5850, Springer, 2009.
Zusammenfassung
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.