VCC verifier

VCC verifier
[Google Scholar] [Website]

Notes: Boogie verifier, Z3 solver, auto-active verification

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.