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. In: Proceedings of Fifth International Workshop on Automated Verification of Critical Systems. Warwick, 2005, s. 101-117.
Název česky
Pattern-Based Verification of Programs with Extended Linear Linked Data Structures
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
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
2005
Strany
101-117
Sborník
Proceedings of Fifth International Workshop on Automated Verification of Critical Systems
Konference
Fifth International Workshop on Automated Verification of Critical Systems, University of Warwick, GB
Místo
Warwick, GB
BibTeX
@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"
}
Nahoru