Michal Moskal - VCC, The Verifying C Compiler

Posted By: Peli de Halleux | Jan 30th @ 2:25 AM | 49,869 Views | 0 Comments
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.

  • 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.

Rating:
3
0
Be the first to comment!
Microsoft Communities