Detail publikace

Abstract Regular Tree Model Checking of Complex Dynamic Data Structures

BOUAJJANI Ahmed, HABERMEHL Peter, ROGALEWICZ Adam a VOJNAR Tomáš. Abstract Regular Tree Model Checking of Complex Dynamic Data Structures. In: Static Analysis. Lecture Notes in Computer Science, roč. 4134. Berlin: Springer Verlag, 2006, s. 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
angličtina
Autoři
Bouajjani Ahmed (UPAR7)
Habermehl Peter (UPAR7)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
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
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, DE
BibTeX
@INPROCEEDINGS{FITPUB8159,
   author = "Ahmed Bouajjani and Peter Habermehl and Adam Rogalewicz and Tom\'{a}\v{s} Vojnar",
   title = "Abstract Regular Tree Model Checking of Complex Dynamic Data Structures",
   pages = "52--70",
   booktitle = "Static Analysis",
   series = "Lecture Notes in Computer Science",
   volume = 4134,
   year = 2006,
   location = "Berlin, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-540-37756-6",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/8159"
}
Nahoru