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

Anglický název

Proving Termination of Tree Manipulating Programs

Jazyk

en

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.

Anglický 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.

Dokumenty

BibTex


@inproceedings{BUT30895,
  author="Peter {Habermehl} and Iosif {Radu} and Adam {Rogalewicz} and Tomáš {Vojnar}",
  title="Proving Termination of Tree Manipulating Programs",
  annote="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.",
  address="Springer Verlag",
  booktitle="Automated Technology for Verification and Analysis",
  chapter="30895",
  edition="LNCS 4762",
  howpublished="print",
  institution="Springer Verlag",
  journal="Lecture Notes in Computer Science (IF 0,513)",
  year="2007",
  month="november",
  pages="145--161",
  publisher="Springer Verlag",
  type="conference paper"
}