VCC is a auto-active program verifier for concurrent C programs based on “two-state invariants” that specify the legal state transitions.

VCC was developed by Microsoft Research and was used for a (partial?) verification of Microsoft’s Hyper-V hypervisor.

VCC is built using the Boogie verifier and Z3 solver.

Papers related to VCC verifier

• Local verification of global invariants in concurrent programs [cohen:cav:2010]
• A precise yet efficient memory model for C [cohen:entcs:2009]
• The Boogie verification debugger [legoues:sefm:2011]
• Verifying the Microsoft Hyper-V hypervisor with VCC [leinenbach:fm:2009]
• Annotation inference for separation logic based verifiers [vogels:fmoods:2011]