Detail publikace

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

VOJNAR, T.; ČEŠKA, M.; ERLEBACH, P. Pattern-Based Verification of Programs with Extended Linear Linked Data Structures. Proceedings of Fifth International Workshop on Automated Verification of Critical Systems. Warwick: 2005. p. 101-117.
Název česky
Pattern-Based Verification of Programs with Extended Linear Linked Data Structures
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Češka Milan, prof. RNDr., CSc.
Erlebach Pavel, Ing., Ph.D.
Klíčová slova

formal verification, program analysis, dynamic linked data structures

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ěř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.

Rok
2005
Strany
101–117
Sborník
Proceedings of Fifth International Workshop on Automated Verification of Critical Systems
Konference
Pátý mezinárodní workshop automatické verifikace kritických systémů, University of Warwick, GB
Místo
Warwick
BibTeX
@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"
}
Nahoru