Detail publikace
Pattern-Based Verification of Programs with Extended Linear Linked Data Structures
formal verification, program analysis, dynamic linked data structures
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.
@article{BUT45072,
author="Tomáš {Vojnar} and Milan {Češka} and Pavel {Erlebach}",
title="Pattern-Based Verification of Programs with Extended Linear Linked Data Structures",
journal="ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE",
year="2006",
volume="2006",
number="145",
pages="113--130",
issn="1571-0661"
}