BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Practical Boogie (on the example of VCC) - Michal Moskal\, MSR Red
 mond
DTSTART:20110811T103000Z
DTEND:20110811T113000Z
UID:TALK32324@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:I’m going to talk about encoding various constructs in Boogi
 e. In particular I’ll focus on object invariants\, as implemented in VCC
 \, and what can be built on them: ownership\, counting permissions for con
 current programs\, recursive data-structures\, and secrecy properties. I
 ’ll also talk about encoding data-types\, termination checking\, and ind
 uction proofs.\n\nVCC is a verifier of complex\, user-supplied properties 
 of concurrent C programs. It builds on top of Boogie\, an intermediate ver
 ification language\, generating verification conditions for various prover
 s including Z3. \n
LOCATION:Small lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR