登陆
注册
工具列表
Tool list
VCC
2020-06-01
195
VCC is a tool that proves correctness of annotated concurrent C programs or finds problems in them.
VCC extends C with design by contract features,like pre-and postcondition as well as type invariants. Annotated programs are translated to logical formulas using the Boogie tool.
VCC is available for non-commercial use,with sources, at our codeplex.
-
A Practical Verification Methodology for Concurrent Programs
We describe a methodology for reasoning about realistic concurrent programs. Our methodology allows ...
-
A Precise Yet Efficient Memory Model For C
We propose a sound typed semantics for C that provides the annotational and computational advantages...
-
Local Verification of Global Invariants in Concurrent Programs
We describe a practical method for reasoning about realistic concurrent programs. Our method allows ...
