Detail publikace

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.
Název česky
Dokazování konečnosti běhu programů manipulujících stromové struktury
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Habermehl Peter
Radu Iosif
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
URL
Klíčová slova

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

Abstrakt

Článek navrhuje metodu automatického dokazování konečnosti běhuprogramů manipulujících stromové struktury, založenou na využití teorieautomatů. Konkrétně je pro úvodní fázi metody, ve které se generujíinvarianty programů, použit abstraktní stromový regulární modelchecking založený na stromových automatech. Pro následnou fáziverifikace konečnosti programů je využit překlad do čítačových automatů.

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, Tokyo, JP
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"
}
Nahoru