VCC: Contract-based Modular Verification of Concurrent C
- Wolfram Schulte
31st International Conference on Software Engineering, ICSE 2009 |
Published by IEEE Computer Society
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.
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 pubs-permissions@ieee.org. By choosing to view this document, you agree to all provisions of the copyright laws protecting it.