Detail publikačního výsledku

Proving Termination of Tree Manipulating Programs

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

Originální název

Proving Termination of Tree Manipulating Programs

Anglický název

Proving Termination of Tree Manipulating Programs

Druh

Stať ve sborníku mimo WoS a Scopus

Originální abstrakt

We consider the termination problem of programs manipulating tree-likedynamic data structures. Our approach is based on anabstract-check-refine loop. We use abstract regular tree model-checkingto infer invariants of the program. Then, we translate the program to acounter automaton  which simulates it. If the counter automatoncan be shown to terminate using existing techniques, the programterminates. If not, we analyze the possible counterexample given by acounter automata termination checker and either conclude that theprogram does not terminate, or else refine the abstraction  andrepeat. We show that the spuriousness problem for lasso-shapedcounterexamples is decidable in some non-trivial cases. We applied themethod successfully on several interesting case studies.

Anglický abstrakt

We consider the termination problem of programs manipulating tree-likedynamic data structures. Our approach is based on anabstract-check-refine loop. We use abstract regular tree model-checkingto infer invariants of the program. Then, we translate the program to acounter automaton  which simulates it. If the counter automatoncan be shown to terminate using existing techniques, the programterminates. If not, we analyze the possible counterexample given by acounter automata termination checker and either conclude that theprogram does not terminate, or else refine the abstraction  andrepeat. We show that the spuriousness problem for lasso-shapedcounterexamples is decidable in some non-trivial cases. We applied themethod successfully on several interesting case studies.

Klíčová slova

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

Klíčová slova v angličtině

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

Autoři

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

Rok RIV

2010

Vydáno

08.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

Svazek

4762

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