Detail publikace

Automata-based Verification of Programs with Tree Updates

IOSIF, R.; VOJNAR, T.; HABERMEHL, P. Automata-based Verification of Programs with Tree Updates. Acta Informatica, 2010, vol. 47, no. 1, p. 1-31. ISSN: 0001-5903.
Název česky
Verifikace programů s operacemi nad vyváženými stromy s využitím automatů
Typ
článek v časopise
Jazyk
anglicky
Autoři
Radu Iosif
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Habermehl Peter
URL
Klíčová slova

Formal verification, symbolic verification, programs handling balanced trees, theory of automata.

Abstrakt

Článek, který je rozšířenou, finální verzí příspěvku původně prezentovaného na TACAS'06, zavádí originální třídu stromových automatů TASC s omezeními nad"velikostí" jednotlivých větví. Tato třída je uzavřena vůči sjednocení,průniku, doplňku, je možné TASC determinizovat a testovat na neprázdnost. Motivací je využitítěchto automatů při symbolické verifikaci programů manipulujícíchvyvážené stromové struktury (AVL stromy, red-black stromy). Pro potřebyverifikace těchto programů je dále zavedena třída omezenýchTASC---rTASC. Ty je možné determinizovat i minimalizovat a jsouuzavřeny vůči všem potřebným operacím nad stromy (včetně stromovýchrotací). Nejsou ale uzavřeny vůči např. doplňku. Je pak navrženaoriginální verifikační metoda založená na využití Hoareových trojic,jež využívá rTASC k reprerezentaci vstupních a výstupních podmínekprogramů a invariantů cyklů. Na rTASC také probíhá výpočet efektůnecyklických úseků programů. Toho, že každý rTASC je TASC se pakvyužívá k ověření platnosti navržených invariantů a podmínek programupomocí testu na inkluzi.

Rok
2010
Strany
1–31
Časopis
Acta Informatica, roč. 47, č. 1, ISSN 0001-5903
BibTeX 
@article{BUT50539,
  author="Iosif {Radu} and Tomáš {Vojnar} and Peter {Habermehl}",
  title="Automata-based Verification of Programs with Tree Updates",
  journal="Acta Informatica",
  year="2010",
  volume="47",
  number="1",
  pages="1--31",
  issn="0001-5903",
  url="http://www.springerlink.com/content/l76231376151vx88/"
}
Nahoru