Detail publikace

Abstract Regular Tree Model Checking of Complex Dynamic Data Structures

BOUAJJANI, A.; HABERMEHL, P.; ROGALEWICZ, A.; VOJNAR, T. Abstract Regular Tree Model Checking of Complex Dynamic Data Structures. In Static Analysis. LNCS 4134. Berlin: Springer Verlag, 2006. p. 52-70. ISBN: 978-3-540-37756-6.
Název česky
Verifikace komplexních dynamických datových struktur za použitím abstraktního regulárního stromového model checkingu
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Bouajjani Ahmed
Habermehl Peter
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
URL
Klíčová slova

Formální verifikace, symbolická verifikace, dynamicé datové struktury, stromové automaty

Abstrakt

Článek se zabývá verifikací programů pracujících s dynamickými datovými strukturami. Každý uzel může obsahovat několik ukazatelů na následující uzly a datovou hodnotu z konečné množiny datových hodnot. Kontrolujeme zakázané manipulace s nulovými a nedefinovanými ukazateli, a dále i tvarové vlastnosti (shape properties) datové struktury. Pro specifikaci těchto vlastností používáme fragment first-order logiky nad grafy. Zakázané stavy popsané v této logice lze automaticky převést do C programu, který je přidán na konec verifikovaného programu. Tímto převedeme problem kontroly datové struktury na problem dosažitelnosti dané řádky v programu. Konfigurace programu, které jsou orientovanými grafy kódujeme jako rozšířené stromové automaty, a příkazy programu jako stromové převodníky. Poté můžeme využít metodu abstract regular tree model checking pro automatickou verifikaci těchto programů. Kompletní metoda byla implementována v prototypovém nástroji a vyzkoušena na několika případových studiích.

Rok
2006
Strany
52–70
Sborník
Static Analysis
Řada
LNCS 4134
ISBN
978-3-540-37756-6
Vydavatel
Springer Verlag
Místo
Berlin
BibTeX 
@inproceedings{BUT30748,
  author="Ahmed {Bouajjani} and Peter {Habermehl} and Adam {Rogalewicz} and Tomáš {Vojnar}",
  title="Abstract Regular Tree Model Checking of Complex Dynamic Data Structures",
  booktitle="Static Analysis",
  year="2006",
  series="LNCS 4134",
  pages="52--70",
  publisher="Springer Verlag",
  address="Berlin",
  isbn="978-3-540-37756-6"
}
Nahoru