Sciweavers

Share
ICSE
2009
IEEE-ACM

VCC: Contract-based modular verification of concurrent C

10 years 10 days ago
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.
Markus Dahlweid, Michal Moskal, Thomas Santen, Ste
Added 19 Feb 2011
Updated 19 Feb 2011
Type Journal
Year 2009
Where ICSE
Authors Markus Dahlweid, Michal Moskal, Thomas Santen, Stephan Tobies, Wolfram Schulte
Comments (0)
books