Intro
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. Annotated programs are translated to logical formulas using the Boogie tool, which passes them to an automated SMT solver Z3 to check their validity.
It is implemented primarily in F# and supports a plugin model. Our daily builds are published here automatically; we strongly encourage using always the latest build.
- You cannot just download the sources an build VCC! See the Build Instructions for information on how to build VCC.
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 within 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. Alternatively one can use Z3 Inspector to perform a live monitoring of proof progress.
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 application of VCC is 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 100 thousand lines of operating system-level C and x64 assembly code, it is therefore not a trivial target.
The verification of Hyper-V is carried out in the project
Verisoft XT, partially funded by the German Ministry of Education and Research (
BMBF). Many features of VCC have been motivated by the complexity of the hypervisor verification.
Features
- soundness -- we're aiming at verification of properties, not bug-finding
- support for concurrency -- operating systems stopped to be single-threaded 20 years ago
- support for 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!
Papers
The first paper, accompanying Wolfram's invited talk, provides a good introduction to VCC. The other three give some more formal, but likely harder to understand, treatment.
- VCC: A Practical System for Verifying Concurrent C. Ernie Cohen, Markus Dahlweid, Mark Hillebrand, Dirk Leinenbach, Michał Moskal, Thomas Santen, Wolfram Schulte, Stephan Tobies. 22nd International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2009), to appear. (LNCS 5674). PDF
- Local Verification of Global Invariants in Concurrent Programs. Ernie Cohen, Michał Moskal, Wolfram Schulte, Stephan Tobies. Draft. January 2010. PDF
- A Practical Verification Methodology for Concurrent Programs. Ernie Cohen, Michał Moskal, Wolfram Schulte, Stephan Tobies. MSR-TR-2009-15. PDF The one above is better.
- A Precise Yet Efficient Memory Model For C. Ernie Cohen, Michał Moskal, Wolfram Schulte, Stephan Tobies. 4th International Workshop on Systems Software Verification (SSV2009). PDF
Wiki pages