Verifying C Programs: A VCC Tutorial

VCC is a verification environment for software written in C. VCC takes a program (annotated with function contracts, state assertions, and type invariants) and attempts to prove that these annotations are cor-rect, i.e. that they hold for every possible program execution. The en-vironment includes tools for monitoring proof attempts and constructing 1 partial counterexample executions for failed proofs. VCC handles fine-grained concurrency and low-level C features, and has been used to verify the functional correctness of tens of thousands of lines of commercial con-current system code. This tutorial describes how to use VCC to verify C code. It covers the annotation language, the verification methodology, and the use of VCC itself.