BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The Relationship Between Separation Logic and Implicit Dynamic Fra
 mes - Dr Alexander Summers\, ETH Zurich
DTSTART:20130821T100000Z
DTEND:20130821T110000Z
UID:TALK46820@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Separation Logic is a popular approach to the formal verificat
 ion of heap-manipulating programs. More recently\, Implicit Dynamic Frames
  has been proposed as an alternative specification logic which is tailored
  for automatic verification based on state-of-the-art first-order solvers 
 such as Z3 (cf. the Chalice and VeriCool tools). In this talk\, I will pre
 sent recent work (in collaboration with Matthew Parkinson) in formally con
 necting the two specification logics for the first time\, and the resultin
 g technical benefits that this yields for both approaches.\n\nThe work has
  been extended since our initial ESOP 2011 paper\, to incorporate a novel 
 semantics for the intuitionistic implication and magic wand connectives wh
 ich works well for both approaches and could lead to better practical impl
 ementations of these (typically unsupported) connectives in future tools. 
 I’ll also discuss some follow-on projects which have been influenced by 
 this connection.\n
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR