BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Practical Techniques for Auto-Active Verification - Nadia Polikarp
 ova\, ETH Zurich
DTSTART:20140709T100000Z
DTEND:20140709T110000Z
UID:TALK53209@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Auto-active verification occupies a niche between fully automa
 tic analysis and interactive proofs: it targets a high degree of automatio
 n (usually powered by SMT solvers)\, while supporting programmer-friendly 
 \nuser interaction through source code annotations. This talk will describ
 e a practical auto-active approach to verifying object-oriented programs a
 nd discuss techniques for making users' interaction with \nauto-active too
 ls more effective.\n\nInvariant-based reasoning about object-oriented prog
 rams becomes challenging in the presence of collaborating objects that nee
 d to maintain global consistency. This talk will present semantic collabor
 ation: a methodology to specify and reason about class invariants that mod
 els dependencies between collaborating objects by semantic means. The meth
 odology is implemented in an auto-active verifier for the Eiffel programmi
 ng language\, and evaluated on several challenge problems and a realistic 
 data structure library.\n\nOne of the biggest remaining obstacles to using
  auto-active verifiers in practice is the quality of feedback they provide
  when a proof attempt fails. The second part of the talk will describe a t
 echnique to generate \nconcrete test cases for programs annotated with com
 plex specifications\, which helps understand and debug failed verification
  attempts.\n\n
LOCATION:Small Lecture Theatre\, Microsoft Research Ltd\, 21 Station Road\
 , Cambridge\, CB1 2FB
END:VEVENT
END:VCALENDAR