Conference paper

 
Habermehl, P., Iosif, R., Rogalewicz, A., Vojnar, T.: Proving Termination of Tree Manipulating Programs, In: Automated Technology for Verification and Analysis, Berlin, DE, Springer, 2007, p. 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
Pages:145-161
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
Year:2007
ISBN:978-3-540-75595-1
Publisher:Springer Verlag
URL:http://www-verimag.imag.fr/index.php?page=techrep-list&lang=fr&long=yes#TR-2007-1-long [HTML]
Keywords
formal verification, program analysis, termination checking, automata theory, tree automata, counter automata
Annotation
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.
BibTeX:
@INPROCEEDINGS{
   author = {Peter Habermehl and Radu Iosif and Adam Rogalewicz and Tomáš
	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 = {http://www.fit.vutbr.cz/research/view_pub.php?id=8510}
}