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.

• Type: Journal
• Year: 2009
• Where: ICSE
• Authors: Markus Dahlweid, Michal Moskal, Thomas Santen, Stephan Tobies, Wolfram Schulte
• Keywords: ICSE 2009, Microsoft Visual Studio, Real-world Production Code, Software Engineering, Sound Verification Methodology