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. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, vol. 2006, no. 145, p. 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
anglicky
Autoři
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Češka Milan, prof. RNDr., CSc.
Erlebach Pavel, Ing., Ph.D.
URL
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ěř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)
BibTeX
@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"
}
Nahoru