VCC: A Verifier for Concurrent C
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.
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.
- Ernie Cohen, Markus Dahlweid, Mark A. Hillebrand, Dirk Leinenbach, Michal Moskal, Thomas Santen, Wolfram Schulte, and Stephan Tobies, VCC: A Practical System for Verifying Concurrent C, in Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009, Springer, 2009
- Ernie Cohen, Michal Moskal, Wolfram Schulte, and Stephan Tobies, Local Verification of Global Invariants in Concurrent Programs, no. MSR-TR-2010-9, 26 January 2010
- Ernie Cohen, Michał Moskal, Wolfram Schulte, and Stephan Tobies, A Precise Yet Efficient Memory Model For C, Elsevier , May 2009
- Ernie Cohen, Michal Moskal, Wolfram Schulte, and Stephan Tobies, A Practical Verification Methodology for Concurrent Programs, no. MSR-TR-2009-2019, February 2009
- Markus Dahlweid, Michal Moskal, Thomas Santen, Stephan Tobies, and Wolfram Schulte, VCC: Contract-based Modular Verification of Concurrent C, in 31st International Conference on Software Engineering, ICSE 2009, IEEE Computer Society, 2008
- Stefan Maus, Michal Moskal, and Wolfram Schulte, Vx86: x86 Assembler Simulated in C Powered by Automated Theorem Proving, in AMAST, Springer, 2008
- K. Rustan M. Leino, Michal Moskal, and Wolfram Schulte, Verification Condition Splitting, Microsoft Research, 2008
- Ernie Cohen, Eyad Alkassar, Vladimir Boyarinov, Markus Dahlweid, Ulan Degenbaev, Mark A. Hillebrand, Bruno Langenstein, Dirk Leinenbach, Michal Moskal, Steven Obua, Wolfgang J. Paul, Hristo Pentchev, Elena Petrova, Thomas Santen, Norbert Schirmer, Sabine Schmaltz, Wolfram Schulte, Andrey Shadrin, Stephan Tobies, Alexandra Tsyban, and Sergey Tverdyshev, Invariants, Modularity, and Rights, in Perspectives of Systems Informatics, 7th International Andrei Ershov Memorial Conference, PSI 2009, Novosibirsk, Russia, June 15-19, 2009. Revised Papers, Springer, 2009
- Sascha Böhme, Michał Moskal, Wolfram Schulte, and Burkhart Wolff, HOL-Boogie — An Interactive Prover-Backend for the Verifying C Compiler, in Journal of Automated Reasoning, Springer Verlag, February 2010
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.
People
People currently working on the VCC project:
- Ernie Cohen, Microsoft Corp.
- Markus Dahlweid, EMIC
- Sebastian Fillinger, RWTH Aachen, intern at EMIC
- Stefan Maus, University of Freiburg, past intern at MSR
- Michał Moskal, EMIC
- Thomas Santen, EMIC
- Wolfram Schulte, MSR
- Stephan Tobies, EMIC
- Herman Venter, MSR
People who used to work on VCC are:
- Matko Botinčan, University of Zagreb, past intern at MSR.
- Lieven Desmet, Katholieke Universiteit Leuven, past intern at EMIC.
