Detail publikace

Pattern-Based Verification of Programs with Extended Linear Linked Data Structures

ČEŠKA Milan, ERLEBACH Pavel a VOJNAR Tomáš. Pattern-Based Verification of Programs with Extended Linear Linked Data Structures. Electronic Notes in Theoretical Computer Science, roč. 2006, č. 145, s. 113-130. ISSN 1571-0661.
Název česky
Pattern-Based Verification of Programs with Extended Linear Linked Data Structures
Typ
článek v časopise
Jazyk
angličtina
Autoři
Češka Milan, prof. RNDr., CSc. (UITS FIT VUT)
Erlebach Pavel, Ing. (UITS FIT VUT)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
URL
Abstrakt

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.

Rok
2006
Strany
113-130
Časopis
Electronic Notes in Theoretical Computer Science, roč. 2006, č. 145, ISSN 1571-0661
Kniha
Proceedings of the 5th International Workshop on Automated Verification of Critical Systems (AVoCS 2005)
Vydavatel
Elsevier Science
BibTeX 
@ARTICLE{FITPUB7985,
   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 = "113--130",
   booktitle = "Proceedings of the 5th International Workshop on Automated Verification of Critical Systems (AVoCS 2005)",
   journal = "Electronic Notes in Theoretical Computer Science",
   volume = 2006,
   number = 145,
   year = 2006,
   ISSN = "1571-0661",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/7985"
}
Nahoru