BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Automating reasoning tasks for separation logic - Juan A. Navarro 
 Pérez\, UCL
DTSTART:20140117T160000Z
DTEND:20140117T170000Z
UID:TALK48635@talks.cam.ac.uk
CONTACT:Jonathan Hayman
DESCRIPTION:One of the main goals of program analysis and verification is 
 to develop fully automated tools that can reason efficiently about as many
  programs as possible. However\, scalable automated reasoning is still amo
 ng the main challenges for programs which operate on user-defined data str
 uctures on the heap.\n\n\nIn this talk I will give an overview of recent w
 ork on the automation of separation logic\, a formalism which has proved q
 uite powerful for reasoning about such data structures. I will introduce t
 he basic techniques behind a decision procedure for entailment checking on
  a fragment of the logic restricted to list segments\, and describe how su
 ch techniques are generalised in two directions: to provide combined reaso
 ning with other theories (SMT)\, and to decide the satisfiability of induc
 tive definitions of arbitrary heap shapes.
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR