VCC: Contract-based Modular Verification of Concurrent C

被引：30

作者：

Dahlweid, Markus ^{[1
]}

Moskal, Michal ^{[1
]}

Santen, Thomas ^{[1
]}

Tobies, Stephan ^{[1
]}

Schulte, Wolfram ^{[2
]}

机构：

[1] European Microsoft Innovat Ctr, Ritterstr 23, D-52072 Aachen, Germany

[2] Microsoft Res, Redmond, WA 98052 USA

来源：

2009 31ST INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, COMPANION VOLUME | 2009年

关键词：

D O I：

10.1109/ICSE-COMPANION.2009.5071046

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

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.

引用

页码：429 / +

页数：2