Conference paper

HABERMEHL Peter, IOSIF Radu, ROGALEWICZ Adam and VOJNAR Tomáš. Proving Termination of Tree Manipulating Programs. In: Automated Technology for Verification and Analysis. Berlin: Springer Verlag, 2007, pp. 145-161. ISBN 978-3-540-75595-1.
Publication language:english
Original title:Proving Termination of Tree Manipulating Programs
Title (cs):Dokazování konečnosti běhu programů manipulujících stromové struktury
Proceedings:Automated Technology for Verification and Analysis
Conference:5th International Symposium on Automated Technology for Verification and Analysis -- ATVA 2007
Series:LNCS 4762
Place:Berlin, DE
Publisher:Springer Verlag
formal verification, program analysis, termination checking, automata theory, tree automata, counter automata
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 analyze 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.
   author = {Peter Habermehl and Radu Iosif and Adam Rogalewicz
	and Tom{\'{a}}{\v{s}} Vojnar},
   title = {Proving Termination of Tree Manipulating Programs},
   pages = {145--161},
   booktitle = {Automated Technology for Verification and Analysis},
   series = {LNCS 4762},
   year = 2007,
   location = {Berlin, DE},
   publisher = {Springer Verlag},
   ISBN = {978-3-540-75595-1},
   language = {english},
   url = {}

Your IPv4 address:
Switch to https