Detail publikace

Proving Termination of Tree Manipulating Programs

HABERMEHL, P.; IOSIF, R.; ROGALEWICZ, A.; VOJNAR, T. Proving Termination of Tree Manipulating Programs. In Automated Technology for Verification and Analysis. LNCS 4762. 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ěhu programů manipulujících stromové struktury, založenou na využití teorie automatů. Konkrétně je pro úvodní fázi metody, ve které se generují invarianty programů, použit abstraktní stromový regulární model checking založený na stromových automatech. Pro následnou fázi verifikace 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
LNCS 4762
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="LNCS 4762",
  pages="145--161",
  publisher="Springer Verlag",
  address="Berlin",
  isbn="978-3-540-75595-1"
}
Nahoru