Detail výsledku

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.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Habermehl Peter
Radu Iosif
Rogalewicz Adam, doc. Mgr., Ph.D.
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
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

URL
Rok
2007
Strany
145–161
Sborník
Automated Technology for Verification and Analysis
Řada
Lecture Notes in Computer Science
Svazek
4762
Konference
5th International Symposium on Automated Technology for Verification and Analysis -- ATVA 2007
ISBN
978-3-540-75595-1
Vydavatel
Springer Verlag
Místo
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"
}
Projekty
Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů, GAČR, Doktorské granty, GD102/05/H050, zahájení: 2005-01-01, ukončení: 2008-12-31, ukončen
Pokročilé formální přístupy v návrhu a automatické verifikaci počítačových systémů, GAČR, Standardní projekty, GA102/07/0322, zahájení: 2007-01-01, ukončení: 2009-12-31, ukončen
Výzkum informačních technologií z hlediska bezpečnosti, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, zahájení: 2007-01-01, ukončení: 2013-12-31, řešení
Výzkumné skupiny
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav inteligentních systémů (UITS)
Nahoru