BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Logic and Semantics Seminar (Computer Laboratory)
SUMMARY:Cyclic Abduction of Inductive Termination Precondi
 tions - James Brotherston\, University College Lon
 don
DTSTART;TZID=Europe/London:20130301T160000
DTEND;TZID=Europe/London:20130301T170000
UID:TALK43756AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/43756
DESCRIPTION:The question "does program P terminate\, given pre
 condition X?" is a \nclassic one in program analys
 is. In this talk\, we aim to go a bit \nfurther an
 d ask the following *abduction* question: "can we 
 find a \nreasonable precondition X under which P t
 erminates?". When one considers \nheap-manipulatin
 g programs\, this problem typically involves inven
 ting the \ninductive definitions of data structure
 s. For example\, a program \nthat traverses "next"
  fields of pointers until it reaches "nil" will te
 rminate \ngiven a heap structured as an acyclic li
 st as input. But given a cyclic list\, it will fai
 l to \nterminate\, and given something that is not
  a list at all\, it will \ntypically encounter a m
 emory fault and crash. \n\nHere we demonstrate a n
 ew heuristic method\, called *cyclic abduction*\, 
 for \nautomatically inferring the inductive defini
 tions of termination \npreconditions for heap-mani
 pulating programs. That is\, given a \nprogram\, t
 his method returns the definition of an inductivel
 y \ndefined predicate in separation logic under wh
 ich the program is \nguaranteed to terminate (with
 out crashing). Cyclic abduction \nessentially work
 s by searching for a *cyclic proof* of termination
  \nof the program\, abducing definitional clauses 
 of the precondition \nas necessary to advance the 
 proof search process. \n\nWe have implemented cycl
 ic abduction in an automated tool\, which is capab
 le\nof finding natural termination preconditions f
 or a range of small programs. The \nabduced predic
 ates may define segmented\, cyclic\, nested\, and/
 or mutually \ndefined data structures. \n\nThis is
  joint work with Nikos Gorogiannis (also at UCL). 
LOCATION:Room TBC.  Microsoft Research\, Station Road
CONTACT:Jonathan Hayman
END:VEVENT
END:VCALENDAR