Detail publikace
Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata
Holík Lukáš, doc. Mgr., Ph.D. (UITS FIT VUT)
Jonsson Bengt (Uppsala)
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT)
Trinh Quy Cong, MSc. (Uppsala)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
Tento text prezentuje obecný rámec pro verifikaci programů s komplexními dynamickými strukturami, jejichž správnost záleží na relaci uspořádání mezi uloženými datovými strukturami. Náš rámec je založen na pojmu lesního automatu jenž dříve vyvinut pro verifikaci programů manipulujících s haldou. V tomto textu rozšiřujeme lesní automaty o omezení mezi datovými elementy přidruženými k uzlům hald reprezentovaných lesními automaty, a navrhujeme nezbytné úpravy všech operací nezbytných pro použití rozšířených lesních automatů v plně automatickém přístupu k verifikaci, jenž je založen na abstraktní interpretaci. Náš přístup jsme implementovali jako rozšíření nástroje Forester, a aplikovali ho na množství programů manipulujících datové struktury, jako jsou různé varianty jednosměrně a dvojsmerně vázaných seznamů, binární vyhledávací stromy, i přeskakované seznamy. Experimenty ukazují, že náš přístup je nejen plně automatický a relativně obecný, ale také efektivní.
@TECHREPORT{FITPUB10405,
author = "A. Parosh Abdulla and Luk\'{a}\v{s} Hol\'{i}k and Bengt Jonsson and Ond\v{r}ej Leng\'{a}l and Cong Quy Trinh and Tom\'{a}\v{s} Vojnar",
title = "Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata",
pages = "1--35",
year = 2013,
location = "FIT-TR-2013-02, Brno, CZ",
publisher = "Faculty of Information Technology BUT",
language = "english",
url = "https://www.fit.vut.cz/research/publication/10405"
}