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ěřujena verifikaci založenou na vzorech. V tomto přístupu se paměťovékonfigurace abstrahují na základě vyhledání podgrafu odpovídajícímudané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ýchkonfiguracích, které za běhu generuje verifikovaný program. Metoda sesoustředí na programy pracující se širokou třídou rozšířenýchlineárních struktur s lineární kostrou (může být i obousměrá nebocyklická) 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 naprvní/poslední prvek atd.). Výsledky získané z prototypové implementacemetody ukazují, že je metoda velice slibná, a motivují k dalšímrozšířením.
@inproceedings{BUT18064,
author="Tomáš {Vojnar} and Milan {Češka} and Pavel {Erlebach}",
title="Pattern-Based Verification of Programs with Extended Linear Linked Data Structures",
booktitle="Proceedings of Fifth International Workshop on Automated Verification of Critical Systems",
year="2005",
pages="101--117",
address="Warwick"
}