Michal Moskal gives us a short introduction at the Verifying C Compiler (VCC) project. VCC is a tool that proves correctness of annotated concurrent C programs or finds problems in them. VCC extends C with design by contract features, like pre- and postcondition as well as type invariants. The current primary goal of the VCC project is to to verify Microsoft Hyper-V. Hyper-V is a hypervisor -- a thin layer of software that sits just above the hardware and beneath one or more operating systems. The Hypervisor verification project is a cooperation between European Microsoft Innovation Center in Aachen, Germany the RiSE group at Microsoft Research in Redmond and the Saarland University in Saarbrücken, Germany.
- Try VCC in your web browser at http://rise4fun.com/vcc !
- VCC slide deck, get the high-level picture and more details,
- VCC home page, all you want to know.
- Unfortunately, there is currently no download available of VCC.
The Research in Software Engineering team (RiSE) coordinates Microsoft's research in Software Engineering in Redmond, USA.