VCC is available for non-commercial use, with sources, at our codeplex site.

Workflow

The work flow is illustrated by the figure below. One starts with annotating the C code with contracts. Contracts are written using C preprocessor macros, so one can get rid of them using a single preprocessor switch and compile the code using one’s favorite C compiler. If the contracts are left in place, VCC when run on a program will report:

• that the program is correct, in which case we’re happy
• that an assertion might fail during execution of the program, in which case we can use Model Viewer (another tool developed withing the VCC project) application to inspect the circumstances in which the assertion might fail
• the prover will diverge–it’s unfortunately the case that verification is undecidable–in which case we can see how did the proof go using the Z3 Axiom Profiler (formerly Z3 Visualizer, yet another VCC project tool), and perhaps make the specification more bearable to the prover

The VCC research project is being developed primarily in European Microsoft Innovation Center in Aachen, Germany and in the RiSE group at Microsoft Research in Redmond.

Hyper-V

The current primary goal of the VCC project is to to verify Microsoft Hyper-V. The Microsoft Hyper-V is a hypervisor — a thin layer of software that sits just above the hardware and beneath one or more operating systems. Its primary job is to provide isolated execution environments called partitions. Each partition is provided with its own set of hardware resources (memory, devices, CPU cycles). A hypervisor is responsible for controlling and arbitrating access to the underlying hardware and in particular for maintaining strong isolation between partitions.

Hyper-V consists of about 60 thousand lines of operating system-level C and x64 assembly code, it is therefore not a trivial target.

Features

• soundness — we are aiming at verification of deep system properties, not bug-finding
• support for concurrency — operating systems stopped to be single-threaded 20 years ago
• modularity — swallowing tens of thousands of lines in one chunk might be hard
• support for low-level C features (bitfields, unions, wrap-around arithmetic) — we are verifying operating systems after all!

Downloads

VCC is available for non-commercial use, with sources, at our codeplex site.

Talks

There are also some slide decks from talks:

• Verifying concurrent C programs with VCC, Boogie and Z3. Workshop on Linking Tools for Verified Software, Microsoft Research Cambridge, November 27-28, 2008. Slides as available as PPT or PDF, but the PDF version doesn’t have inter-slide transitions.