Detail publikace

Proving Termination of Tree Manipulating Programs

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

Originální název

Proving Termination of Tree Manipulating Programs

Typ

článek ve sborníku mimo WoS a Scopus

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

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

Autoři

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

Rok RIV

2007

Vydáno

8. 11. 2007

Nakladatel

Springer Verlag

Místo

Berlin

ISBN

978-3-540-75595-1

Kniha

Automated Technology for Verification and Analysis

Edice

Lecture Notes in Computer Science

Strany od

145

Strany do

161

Strany počet

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"
}