Detail publikačního výsledku

Proving Termination of Tree Manipulating Programs

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

Original Title

Proving Termination of Tree Manipulating Programs

English Title

Proving Termination of Tree Manipulating Programs

Type

Paper in proceedings outside WoS and Scopus

Original Abstract

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.

English abstract

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.

Keywords

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

Key words in English

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

Authors

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

RIV year

2010

Released

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

Volume

4762

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

Full text in the Digital Library

http://hdl.handle.net/

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