Detail publikace

Automata-based Verification of Programs with Tree Updates

HABERMEHL, P.; IOSIF, R.; VOJNAR, T. Automata-based Verification of Programs with Tree Updates. Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2006. p. 350-364. ISBN: 978-3-540-33056-1.
Název česky
Verifikace programů s operacemi nad vyváženými stromy s využitím automatů
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Habermehl Peter
Radu Iosif
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
URL
Klíčová slova

Formální verifikace, symbolická verifikace, programy nad vyváženými stromy, teorie automatů.

Abstrakt

Článek 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
2006
Strany
350–364
Sborník
Tools and Algorithms for the Construction and Analysis of Systems
Řada
Lecture Notes in Computer Science
Svazek
3920
Konference
The European Joint Conference on Theory and Practice of Software -- ETAPS'06 / 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems -- TACAS'06, Vienna, AT
ISBN
978-3-540-33056-1
Vydavatel
Springer Verlag
Místo
Berlin
BibTeX 
@inproceedings{BUT30893,
  author="Peter {Habermehl} and Iosif {Radu} and Tomáš {Vojnar}",
  title="Automata-based Verification of Programs with Tree Updates",
  booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
  year="2006",
  series="Lecture Notes in Computer Science",
  volume="3920",
  pages="350--364",
  publisher="Springer Verlag",
  address="Berlin",
  isbn="978-3-540-33056-1",
  url="http://www-verimag.imag.fr/TR/TR-2005-16.ps"
}
Nahoru