BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The Ramifications of Sharing in Data Structures - Jules Villard\, 
 University College London
DTSTART:20130410T090000Z
DTEND:20130410T100000Z
UID:TALK43931@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Programs manipulating mutable data structures with intrinsic s
 haring present a challenge for modular verification.  Deep aliasing inside
  data structures dramatically complicates reasoning in isolation over part
 s of these objects because changes to one part of the structure (say\, the
  left child of a dag node) can affect other parts (the right child or some
  of its descendants) that may point into it.  The result is that finding i
 ntuitive and compositional proofs of correctness is usually a struggle.  W
 e propose a compositional proof system that enables local reasoning in the
  presence of sharing.\n\nWhile the AI "frame problem" elegantly captures t
 he reasoning required to verify programs without sharing\, we contend that
  natural reasoning about programs with sharing instead requires an answer 
 to a different and more challenging AI problem\, the "ramification problem
 ": reasoning about the indirect consequences of actions.  Accordingly\, we
  present a Ramify proof rule that attacks the ramification problem head-on
  and show how to reason with it.  Our framework is valid in any separation
  logic and permits sound compositional and local reasoning in the context 
 of both specified and unspecified sharing.  This talk will be illustrated 
 by proofs of examples manipulating dags\, graphs\, and overlaid data struc
 tures.\n
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR