Články v časopisech

Habermehl, P., Iosif, R., Vojnar, T.: Automata-based Verification of Programs with Tree Updates, In: Acta Informatica, roč. 47, č. 1, 2010, DE, s. 1-31, ISSN 0001-5903
Jazyk publikace:angličtina
Název publikace:Automata-based Verification of Programs with Tree Updates
Název (cs):Verifikace programů s operacemi nad vyváženými stromy s využitím automatů
Strany:1-31
Místo vydání:DE
Rok:2010
Časopis:Acta Informatica, roč. 47, č. 1, DE
ISSN:0001-5903
URL:http://www.springerlink.com/content/l76231376151vx88/ [HTML]
Klíčová slova
Formal verification, symbolic verification, programs handling balanced trees, theory of automata.
Anotace
Č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ích vyvážené stromové struktury (AVL stromy, red-black stromy). Pro potřeby verifikace těchto programů je dále zavedena třída omezených TASC---rTASC. Ty je možné determinizovat i minimalizovat a jsou uzavřeny vůči všem potřebným operacím nad stromy (včetně stromových rotací). Nejsou ale uzavřeny vůči např. doplňku. Je pak navržena originá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ínek programů a invariantů cyklů. Na rTASC také probíhá výpočet efektů necyklických úseků programů. Toho, že každý rTASC je TASC se pak využívá k ověření platnosti navržených invariantů a podmínek programu pomocí testu na inkluzi.
BibTeX:
@ARTICLE{
   author = {Peter Habermehl and Radu Iosif and Tomáš Vojnar},
   title = {Automata-based Verification of Programs with Tree Updates},
   pages = {1--31},
   journal = {Acta Informatica},
   volume = {47},
   number = {1},
   year = {2010},
   ISSN = {0001-5903},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php?id=9166}
}

Vaše IPv4 adresa: 54.224.75.101
Přepnout na IPv6 spojení

DNSSEC [dnssec]