BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Graph-Based Reasoning in Separation Logic for Fun and Profit - Chr
 istoph Haase\, LSV at ENS Cachan
DTSTART:20130405T090000Z
DTEND:20130405T100000Z
UID:TALK43913@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:In this talk\, I will present a graph-based approach to reason
 ing in a fragment of Separation Logic with pointers and linked lists which
  gives new complexity bounds and new algorithms for standard reasoning pro
 cedures outperforming state-of-the-art reasoners up to several orders of m
 agnitude. Separation Logic is an extension of Hoare logic that enables the
  efficient verification of programs that manipulate dynamically allocated 
 data structures. Over the last couple of years\, fragments of Separation L
 ogic with decidable inference problems have successfully been employed in 
 tools such as Smallfoot\, SpaceInvader or SLAyer to automatically verify i
 ndustrial low-level systems code. The applicability and scalability of the
 se tools heavily depends on the computational costs of the underlying reas
 oning procedures. In the aforementioned tools\, the implemented reasoning 
 procedures for the fragment of Separation Logic with pointers and linked l
 ists proceed via a syntactic proof search\, which gives a worst-case expon
 ential running time. I will present a recently introduced approach to enta
 ilment checking in this fragment which is based on graph-theoretic methods
  and allows for polynomial-time reasoning. Alongside with settling an open
  problem about the complexity of entailment in this fragment and providing
  highly competitive reasoning procedures\, this approach also yields nice 
 algorithms for other reasoning problems such as frame inference. I will co
 nclude my talk discussing limitations and possible directions for future w
 ork.
LOCATION:Auditorium\, Microsoft Research Ltd\, 21 Station Road\, Cambridge
 \, CB1 2FB
END:VEVENT
END:VCALENDAR