Sciweavers

ATVA
2007
Springer

Proving Termination of Tree Manipulating Programs

14 years 5 months ago
Proving Termination of Tree Manipulating Programs
Abstract. We consider the termination problem of programs manipulating treelike dynamic data structures. Our approach is based on a counter-example guided ion refinement loop. We use abstract regular tree model-checking to infer invariants of the program. Then, we translate the program to a counter automaton (CA) which simulates it. If the CA can be shown to terminate using existing techniques, the program terminates. If not, we analyse the possible counterexample given by a CA termination checker and either conclude that the program does not e, 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.
Peter Habermehl, Radu Iosif, Adam Rogalewicz, Tom&
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where ATVA
Authors Peter Habermehl, Radu Iosif, Adam Rogalewicz, Tomás Vojnar
Comments (0)