Result Details

Proving Termination of Tree Manipulating Programs

HABERMEHL, P.; IOSIF, R.; ROGALEWICZ, A.; VOJNAR, T. Proving Termination of Tree Manipulating Programs. Automated Technology for Verification and Analysis. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2007. p. 145-161. ISBN: 978-3-540-75595-1.
Type
conference paper
Language
English
Authors
Habermehl Peter
Radu Iosif
Rogalewicz Adam, doc. Mgr., Ph.D.
Vojnar Tomáš, prof. Ing., Ph.D., DITS (FIT)
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

URL
Published
2007
Pages
145–161
Proceedings
Automated Technology for Verification and Analysis
Series
Lecture Notes in Computer Science
Volume
4762
Conference
5th International Symposium on Automated Technology for Verification and Analysis -- ATVA 2007
ISBN
978-3-540-75595-1
Publisher
Springer Verlag
Place
Berlin
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"
}
Projects
Advanced Formal Approaches in the Design and Verification of Computer-Based Systems, GACR, Standardní projekty, GA102/07/0322, start: 2007-01-01, end: 2009-12-31, completed
Integrated approach to education of PhD students in the area of parallel and distributed systems, GACR, Doktorské granty, GD102/05/H050, start: 2005-01-01, end: 2008-12-31, completed
Security-Oriented Research in Information Technology, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, start: 2007-01-01, end: 2013-12-31, running
Research groups
Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)
Departments
Department of Intelligent Systems (DITS)
Back to top