Practical Boogie (on the example of VCC)

  • Michal Moskal | MSR, Redmond

I’m going to talk about encoding various constructs in Boogie. In particular I’ll focus on object invariants, as implemented in VCC, and what can be built on them: ownership, counting permissions for concurrent programs, recursive data-structures, and secrecy properties. I’ll also talk about encoding data-types, termination checking, and induction proofs.

VCC is a verifier of complex, user-supplied properties of concurrent C programs. It builds on top of Boogie, an intermediate verification language, generating verification conditions for various provers including Z3.

    • Portrait of Michal Moskal

      Michal Moskal

      Principal Research Software Development Engineer

Watch Next