LFCS Seminar: James Brotherston
Cyclic Abduction of Inductive Safety & Termination Preconditions
What 


When 
May 08, 2013 from 04:00 PM to 05:00 PM 
Where  IF 4.02 
Add event to calendar 
vCal iCal 
Whether a given program ever encounters a memory fault, or indeed ever terminates, are natural (and undecidable) problems in program analysis. Usually, we are interested in establishing such safety and termination properties under a given "precondition" in logic that expresses some known initial conditions about the program.
However, in this talk, I will go a step further and consider the problem of *inferring* a reasonable precondition under which a given program is memorysafe and/or terminates. When one considers heapmanipulating programs, this problem typically involves inventing the inductive definitions of data structures. For example, a program that traverses a list will:
 terminate safely, given an acyclic list as input;
 run safely but not terminate, given a cyclic list as input;
 encounter a memory fault and crash, given something that is in no way a list as input.
Here I demonstrate a new method, called *cyclic abduction*, for
automatically inferring the inductive definitions of safety and termination preconditions for heapmanipulating programs. That is, given a program, this method attempts to invent the definition of an inductively defined predicate in separation logic under which the program is guaranteed safe and/or terminating. Cyclic abduction
essentially works by searching for a *cyclic proof* of safety / termination, abducing definitional clauses of the precondition as necessary to advance the proof search process.
Our cyclic abduction method has been implemented in the Cyclist theorem
prover, and tested on a suite of small programs. The abduced predicates may define segmented, cyclic, nested, and/or mutually defined data structures.
This is joint work with Nikos Gorogiannis (also at UCL).