Publication Details
Proving Termination of Tree Manipulating Programs
Iosif Radu (VERIMAG)
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
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.
@INPROCEEDINGS{FITPUB8510, 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 = "Lecture Notes in Computer Science", volume = 4762, year = 2007, location = "Berlin, DE", publisher = "Springer Verlag", ISBN = "978-3-540-75595-1", language = "english", url = "https://www.fit.vut.cz/research/publication/8510" }