@inproceedings{dahlweid2009vcc,
author = {Dahlweid, Markus and Moskal, Michal and Santen, Thomas and Tobies, Stephan and Schulte, Wolfram},
title = {VCC: Contract-based modular verification of concurrent C},
booktitle = {ICSE Companion},
year = {2009},
month = {May},
abstract = {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 counter-examples 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.},
publisher = {IEEE},
url = {http://approjects.co.za/?big=en-us/research/publication/vcc-contract-based-modular-verification-of-concurrent-c-2/},
pages = {429-430},
isbn = {978-1-4244-3494-7},
edition = {ICSE Companion},
}