Detail publikace

Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata

ABDULLA Parosh A., HOLÍK Lukáš, JONSSON Bengt, LENGÁL Ondřej, TRINH Quy Cong a VOJNAR Tomáš. Verification of Heap Manipulating Programs with Ordered Data by Extended Forest Automata. In: Proceedings of ATVA'13. Heidelberg: Springer Verlag, 2013, s. 224-239. ISBN 978-3-319-02443-1.
Název česky
Použití rozšířených lesních automatů pro verifikaci programů manipulujících s haldou s uspořádáním nad datovými elementy
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
Abdulla Parosh A. (Uppsala)
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)
Abstrakt

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í.

Rok
2013
Strany
224-239
Sborník
Proceedings of ATVA'13
Konference
11th International Symposium on Automated Technology for Verification and Analysis -- ATVA'13, 15th International Workshop on Verification of Infinite-State Systems -- INFINITY'13, 2nd International Workshop on Trends in Tree Automata and Tree Transducers -- TTATT'13, Historical Campus, Vietnam National University, 19 Le Thanh Tong st., Hoan Kiem dist., Hanoi, VN
ISBN
978-3-319-02443-1
Vydavatel
Springer Verlag
Místo
Heidelberg, DE
BibTeX 
@INPROCEEDINGS{FITPUB10385,
   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 = "224--239",
   booktitle = "Proceedings of ATVA'13",
   year = 2013,
   location = "Heidelberg, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-319-02443-1",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/10385"
}
Nahoru