BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Steps toward usable verification - Francesco Logozzo\, MSR Redmond
DTSTART:20140710T090000Z
DTEND:20140710T100000Z
UID:TALK53249@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:First\, I will provide some background information on CodeCont
 racts\, the language-agnostic specification language of .NET 4.x\, and on 
 Clousot\, the companion abstract interpretation-based verifier. I will exp
 lain why we chose abstract interpretation instead of\, e.g.\, using a theo
 rem prover and discuss our experience with its adoption both inside and ou
 tside the company.\nThen\, I will cover topics that make the verification 
 usable by the working programmers: inference of necessary preconditions\, 
 verified code repairs\, refactoring with contracts\, and verification modu
 lo versions. En passant\, I will present a generalization of Hoare Logic\,
  Algebraic Hoare Logic\, and show how the usual conjunction and disjunctio
 n rules require extra hypotheses to ensure soundness.\n
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR