Detail publikace

Automata-based Verification of Programs with Tree Updates

HABERMEHL Peter, IOSIF Radu a VOJNAR Tomáš. Automata-based Verification of Programs with Tree Updates. Verimag Technical Report number TR-2005-16, Grenoble: VERIMAG, 2005.
Název česky
Verifikace programů manipulujících stromové struktury s využitím teorie automatů
Typ
technická zpráva
Jazyk
angličtina
Autoři
Habermehl Peter (UPAR7)
Iosif Radu (VERIMAG)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
Klíčová slova

formální verifikace, symbolické metody, teorie automatů, stromové utomaty, automaty s kvantitativními omezeními

Abstrakt

Článek zavádí novou třídu stromových automatů rozšířených o určitou formu kvantitaivních omezení nad velikostí přijímaných stromů a jejich podstromů. Je ukázáno, že navržená třída má celou řadu  žádoucích jazykově-teoretických vlastností (uzavřenost, rozhodnutelnost). Tato třída je motivována využitím v automatizované verifikaci programů manipulujících vyvážené stromové struktury (Red-Black trees, AVL trees). Je ukázáno, že operace používané pro manipulaci takových struktur lze realizovat nad vhodně zvolenou podtřídou navržených stromových automatů. To tvoří základ pro semi-automatickou metodu formální verifikace programů manipulujících zmíněné datové struktur, jež se velmi často používají v kritických programových dílech(operační a řídicí systémy).

Rok
2005
Strany
28
Vydavatel
VERIMAG
Místo
Verimag Technical Report number TR-2005-16, Grenoble, FR
BibTeX
@TECHREPORT{FITPUB7958,
   author = "Peter Habermehl and Radu Iosif and Tom\'{a}\v{s} Vojnar",
   title = "Automata-based Verification of Programs with Tree Updates",
   pages = 28,
   year = 2005,
   location = "Verimag Technical Report number TR-2005-16, Grenoble, FR",
   publisher = "VERIMAG",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/7958"
}
Nahoru