Intro

VCC is a mechanical verifier for concurrent C programs. VCC takes a C program, annotated with function specifications, data invariants, loop invariants, and ghost code, and tries to prove these annotations correct. If it succeeds, VCC promises that your program actually meets its specifications.

Features

• VCC is sound -- if VCC verifies your program, it really is correct (modulo bugs in VCC itself).
• VCC verification is modular -- VCC verifies your program one function/type definition at a time, using only the specifications of the functions it calls and the data structures it uses. This means that you can verify your code even if the functions you call haven't been written yet.
• VCC supports concurrency -- you can use VCC to verify programs that use both coarse-grained and fine-grained concurrency. You can even use it to verify your concurrency control primitives. Verifying a function implicitly guarantees its thread safety in any concurrent environment that respects the
• VCC supports low-level C features (e.g. bitfields, unions, wrap-around arithmetic).

The work flow is illustrated in the figure below. You start by annotating your C code with contracts that describe both what your program is supposed to do and (certain aspects of) why you think that it works. Contracts are written using C preprocessor macros, so you can get rid of them using a single preprocessor switch and compile the code using your favorite C compiler. Annotated programs are translated to logical formulas using the Boogie tool, which passes them to an automated theorem prover (Z3) to check their validity. VCC is implemented primarily in F#, and supports a plugin model.

When VCC is run, several outcomes are possible:

• VCC reports that the program is correct, in which the program is guaranteed to satisfy all of the annotations.
• VCC reports that it is unable to verify the correctness of one or more of the annotations, in which case you can use the VCC Model Viewer to inspect how VCC thinks your program (or your description of why it works) might fail.
• the theorem prover might diverge, in which case you can use use the VCC Inspector to monitor proof progress (to see which part of the program is causing the verifier to get stuck) or the Z3 Axiom Profiler to see how the prover is spending its time.

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

Papers

• Verifying Concurrent C Programs with VCC. Ernie Cohen, Mark Hillebrand, Michał Moskal, Wolfram Schulte, Stephan Tobies. PDF (2-column, ~25 pages) PDF (1-column, ~65pages) PDF (screen-reading) (A working draft of VCC tutorial - a recommended place to start!)
• 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). (LNCS 5674). PDF (Provides a good overall system description of VCC, the paper to cite for VCC)
• Local Verification of Global Invariants in Concurrent Programs. Ernie Cohen, Michał Moskal, Wolfram Schulte, Stephan Tobies. Computer Aided Verification (CAV2010). PDF (The best description of the underlying methodology)
• A Practical Verification Methodology for Concurrent Programs. Ernie Cohen, Michał Moskal, Wolfram Schulte, Stephan Tobies. MSR-TR-2009-15. PDF (The methodological description is out-of-date, but this provides more detail on how programs are actually verified).
• 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 (Describes the VCC typestate)

Also check out papers about VCC Applications!

Getting Started

You get a taste of VCC by running it in your browser from RiSE4Fun website

Daily builds are published here automatically; we strongly encourage always using the latest build.

• Consult the Install page before installing VCC for the first time.

• You can also download the sources and build VCC yourself. (See the Build Instructions.)

• We strongly recommend working through the VCC tutorial (above).

• You can also download some Samples. Many more examples can be found in the VCC source distribution tree, or in the samples package that can be installed after installing VCC (see "All Programs -> Microsoft Research Vcc -> (Re-)Install Samples")

Wiki pages

• Concepts - root of the documentation tree
• VCC2 Glossary - A simple glossary of VCC related terms
• Annotation FAQ - A dummy's guide to the VCC annotation language
• Compiler messages: Compiler assertions, Warnings, Errors
• Unsupported C Features