Publication detail

Proving Termination of Tree Manipulating Programs

HABERMEHL, P. IOSIF, R. ROGALEWICZ, A. VOJNAR, T.

Original Title

Proving Termination of Tree Manipulating Programs

Type

conference paper

Language

English

Original Abstract

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.

Keywords

formal verification, program analysis, termination checking, automata theory, tree automata, counter automata

Authors

HABERMEHL, P.; IOSIF, R.; ROGALEWICZ, A.; VOJNAR, T.

RIV year

2007

Released

8. 11. 2007

Publisher

Springer Verlag

Location

Berlin

ISBN

978-3-540-75595-1

Book

Automated Technology for Verification and Analysis

Edition

LNCS 4762

Pages from

145

Pages to

161

Pages count

17

BibTex

@inproceedings{BUT30895,
  author="Peter {Habermehl} and Iosif {Radu} and Adam {Rogalewicz} and Tomáš {Vojnar}",
  title="Proving Termination of Tree Manipulating Programs",
  booktitle="Automated Technology for Verification and Analysis",
  year="2007",
  series="LNCS 4762",
  pages="145--161",
  publisher="Springer Verlag",
  address="Berlin",
  isbn="978-3-540-75595-1"
}