Abstract

The question “does program P terminate, given precondition X?” is a classic one in program analysis. In this talk, we aim to go a bit further and ask the following abduction question: “can we find a reasonable precondition X under which P terminates?”. When one considers heap-manipulating programs, this problem typically involves inventing the inductive definitions of data structures. For example, a program that traverses “next” fields of pointers until it reaches “nil” will terminate given a heap structured as an acyclic list as input. But given a cyclic list, it will fail to terminate, and given something that is not a list at all, it will typically encounter a memory fault and crash.

Here we demonstrate a new heuristic method, called cyclic abduction, for automatically inferring the inductive definitions of termination preconditions for heap-manipulating programs. That is, given a program, this method returns the definition of an inductively defined predicate in separation logic under which the program is guaranteed to terminate (without crashing). Cyclic abduction essentially works by searching for a cyclic proof of termination of the program, abducing definitional clauses of the precondition as necessary to advance the proof search process.

We have implemented cyclic abduction in an automated tool, which is capable of finding natural termination preconditions for a range 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 ).