Practical Boogie (on the example of VCC)

Опубликовано 17 августа 2016, 3:07

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.