Personal tools
You are here: Home Events LFCS Seminars-Folder LFCS Seminar: James Brotherston

LFCS Seminar: James Brotherston

— filed under:

Cyclic Abduction of Inductive Safety & Termination Preconditions

  • LFCS Seminar
When May 08, 2013
from 04:00 PM to 05:00 PM
Where IF 4.02
Add event to calendar vCal

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 memory-safe and/or terminates. When one considers heap-manipulating 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 heap-manipulating 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).

Document Actions