Michal Moskal - VCC, The Verifying C Compiler

22 minutes, 4 seconds

Download

Right click “Save as…”

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.

The Research in Software Engineering team (RiSE) coordinates Microsoft's research in Software Engineering in Redmond, USA.

Tags:

Follow the discussion

Comments closed

Comments have been closed since this content was published more than 30 days ago, but if you'd like to continue the conversation, please create a new thread in our Forums, or Contact Us and let us know.