BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Automating Separation Logic Reasoning - Juan Antonio Navarro Pére
 z\, UCL
DTSTART:20121126T140000Z
DTEND:20121126T150000Z
UID:TALK41096@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Program analysis crucially depends on our ability to symbolica
 lly describe and manipulate sets of program behaviours in a mechanical way
 . Separation logic provides a promising foundation for reasoning about dyn
 amic memory allocation in computer programs\, but the development of effic
 ient inference tools for separation logic remains a challenging problem. I
 n this talk I will describe how my work led to the design of an efficient\
 , sound and complete automated theorem prover for checking the validity of
  entailments in a fragment of separation logic.\n\nOur prover is built fro
 m a modular integration of separation logic techniques---to reason about t
 he shape of structures in memory---and superposition calculus---to reason 
 about equality/aliasing between program variables. I will also present som
 e empirical evaluation of the efficiency of this procedure\, which transla
 ted into speedups of several orders of magnitude with respect to previous 
 work\, and discuss the directions in which I'm currently working to furthe
 r generalise these\ntechniques. \n
LOCATION:Large lecture theatre\, Microsoft Research Ltd\, 7 J J Thomson Av
 enue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR