University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Cyclic Abduction of Inductive Termination Preconditions

Cyclic Abduction of Inductive Termination Preconditions

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Jonathan Hayman.

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 ).

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2019 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity