VCC: Contract-based Modular Verification of Concurrent C

Most system level software is written in C and executed concurrently. Because such software is often critical for system reliability, it is an ideal target for formal verification.

Annotated C and the Verified C Compiler (VCC) form the first modular sound verification methodology for concurrent C that scales to real-world production code. VCC

is integrated in Microsoft Visual Studio and it comes with support for verification debugging: an explorer for counterexamples of failed proofs helps to find errors in code or specifications, and a prover log analyzer helps debugging proof attempts that exhaust available resources (memory, time). VCC is currently used to verify the core of Microsoft

Hyper-V, consisting of 50,000 lines of system-level C code.

PDF file

In  31st International Conference on Software Engineering, ICSE 2009

Publisher  IEEE Computer Society
Copyright © 2007 IEEE. Reprinted from IEEE Computer Society. This material is posted here with permission of the IEEE. Internal or personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution must be obtained from the IEEE by writing to By choosing to view this document, you agree to all provisions of the copyright laws protecting it.


> Publications > VCC: Contract-based Modular Verification of Concurrent C