Detail publikace
Pattern-Based Verification of Programs with Extended Linear Linked Data Structures
Erlebach Pavel, Ing. (UITS FIT VUT)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
Tento článek se zabývá problémem automatické verifikace programů pracujících s dynamickými datovými strukturami. Konkrétně se zaměřuje na verifikaci založenou na vzorech. V tomto přístupu se paměťové konfigurace abstrahují na základě vyhledání podgrafu odpovídajícímu danému vzoru. Článek rozšiřuje poznání v této oblasti představením plně automatického a efektivního způsobu detekovaní vzorů v paměťových konfiguracích, které za běhu generuje verifikovaný program. Metoda se soustředí na programy pracující se širokou třídou rozšířených lineárních struktur s lineární kostrou (může být i obousměrá nebo cyklická) případně s dalšími definovanými ukazateli, což zahrnuje velké množství prakticky používaných datových struktur (jako seznamy, obousměrně vázané seznamy, cyklické seznamy, seznamy s ukazateli na první/poslední prvek atd.). Výsledky získané z prototypové implementace metody ukazují, že je metoda velice slibná, a motivují k dalším rozšířením.
@INPROCEEDINGS{FITPUB7888, author = "Milan \v{C}e\v{s}ka and Pavel Erlebach and Tom\'{a}\v{s} Vojnar", title = "Pattern-Based Verification of Programs with Extended Linear Linked Data Structures", pages = "101--117", booktitle = "Proceedings of Fifth International Workshop on Automated Verification of Critical Systems", year = 2005, location = "Warwick, GB", language = "english", url = "https://www.fit.vut.cz/research/publication/7888" }