VCC 2.1.40920.0

VCC was developed to be a mechanical verifier for concurrent C programs. VCC takes a C program, annotated with function specifications, data invariants, loop invariants, and ghost code, and tries to prove these annotations correct. If it succeeds, VCC promises that your program actually meets its specifications. The work flow is illustrated in the figure below. You start by annotating your C code with contracts that describe both what your program is supposed to do and (certain aspects of) why you think that it works. Contracts are written using C preprocessor macros, so you can get rid of them using a single preprocessor switch and compile the code using your favorite C compiler. Annotated programs are translated to logical formulas using the Boogie tool, which passes them to an automated theorem prover (Z3) to check their validity. VCC is implemented primarily in F#, and supports a plugin model. NOTE: Non-Commercial Use Only · VCC is sound — if VCC verifies your program, it really is correct (modulo bugs in VCC itself). · VCC verification is modular — VCC verifies your program one function/type definition at a time, using only the specifications of the functions it calls and the data structures it uses. This means that you can verify your code even if the functions you call haven’t been written yet. · VCC supports concurrency — you can use VCC to verify programs that use both coarse-grained and fine-grained concurrency. You can even use it to verify your concurrency control primitives. · VCC supports low-level C features (bitfields, unions, wrap-around arithmetic) — we are verifying operating systems after all!