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

article in a collection out of WoS and Scopus

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

Lecture Notes in Computer Science

Pages from

145

Pages to

161

Pages count

17

URL

http://www-verimag.imag.fr/index.php?page=techrep-list&lang=fr&long=yes#TR-2007-1-long

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="Lecture Notes in Computer Science",
  volume="4762",
  pages="145--161",
  publisher="Springer Verlag",
  address="Berlin",
  isbn="978-3-540-75595-1",
  url="http://www-verimag.imag.fr/index.php?page=techrep-list&lang=fr&long=yes#TR-2007-1-long"
}