Boogie verifier

[Google Scholar] [Website]

Notes: permission logic, Spec-sharp project, intermediate verification language, verification condition generator

Boogie is an intermediate verification language and verification condition generator developed by Microsoft Research. Originally, part of the Spec# project though it has taken on a life of its own.


Auto active verification, CIVL verifier, Corral verifier, Intermediate verification language, SMACK verifier, Spec# project, VCC verifier, Verification condition generator