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.
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]