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. Static Analysis. Lecture Notes in Computer Science. 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ýmistrukturami. 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ánna konec verifikovaného programu. Tímto převedeme problem kontrolydatové struktury na problem dosažitelnosti dané řádky v programu.Konfigurace programu, které jsou orientovanými grafy kódujeme jakorozšířené stromové automaty, a příkazy programu jako stromovépřevodníky. Poté můžeme využít metodu abstract regular tree modelchecking pro automatickou verifikaci těchto programů. Kompletní metodabyla implementována v prototypovém nástroji a vyzkoušena na několikapřípadových studiích.

Rok
2006
Strany
52–70
Sborník
Static Analysis
Řada
Lecture Notes in Computer Science
Svazek
4134
Konference
13th International Static Analysis Symposium -- SAS 2006, Seoul, KR
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="Lecture Notes in Computer Science",
  volume="4134",
  pages="52--70",
  publisher="Springer Verlag",
  address="Berlin",
  isbn="978-3-540-37756-6",
  url="http://www.fit.vutbr.cz/~rogalew/pubs/artmc_pointers.FULL.pdf"
}
Nahoru