Proving Termination of Tree Manipulating Programs

We consider the termination problem of programs manipulating tree-like dynamic data structures. Our approach is based on an abstract-check-refine loop. We use abstract regular tree model-checking to infer invariants of the program. Then, we translate the program to a counter automaton which simulates it. If the counter automaton can be shown to terminate using existing techniques, the program terminates. If not, we analyse the possible counterexample given by a counter automata termination checker and either conclude that the program does not terminate, or else refine the abstraction and repeat. We show that the spuriousness problem for lasso-shaped counterexamples is decidable in some non-trivial cases. We applied the method successfully on several interesting case studies.

Joint work with: Peter Habermehl (LIAFA, Paris/LSV, Cachan), Radu Iosif (Verimag, Grenoble), and Adam Rogalewicz (FIT BUT, Brno/Verimag, Grenoble).