BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Cyclic Abduction of Inductive Termination Preconditions - James Br
 otherston\, University College London
DTSTART:20130301T160000Z
DTEND:20130301T170000Z
UID:TALK43756@talks.cam.ac.uk
CONTACT:Jonathan Hayman
DESCRIPTION:The question "does program P terminate\, given precondition X?
 " is a \nclassic one in program analysis. In this talk\, we aim to go a bi
 t \nfurther and ask the following *abduction* question: "can we find a \nr
 easonable precondition X under which P terminates?". When one considers \n
 heap-manipulating programs\, this problem typically involves inventing the
  \ninductive definitions of data structures. For example\, a program \ntha
 t traverses "next" fields of pointers until it reaches "nil" will terminat
 e \ngiven a heap structured as an acyclic list as input. But given a cycli
 c list\, it will fail to \nterminate\, and given something that is not a l
 ist at all\, it will \ntypically encounter a memory fault and crash. \n\nH
 ere we demonstrate a new heuristic method\, called *cyclic abduction*\, fo
 r \nautomatically inferring the inductive definitions of termination \npre
 conditions for heap-manipulating programs. That is\, given a \nprogram\, t
 his method returns the definition of an inductively \ndefined predicate in
  separation logic under which the program is \nguaranteed to terminate (wi
 thout crashing). Cyclic abduction \nessentially works by searching for a *
 cyclic proof* of termination \nof the program\, abducing definitional clau
 ses of the precondition \nas necessary to advance the proof search process
 . \n\nWe have implemented cyclic abduction in an automated tool\, which is
  capable\nof finding natural termination preconditions for a range of smal
 l programs. The \nabduced predicates may define segmented\, cyclic\, neste
 d\, and/or mutually \ndefined data structures. \n\nThis is joint work with
  Nikos Gorogiannis (also at UCL). 
LOCATION:Room TBC.  Microsoft Research\, Station Road
END:VEVENT
END:VCALENDAR