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",
url="http://www.sciencedirect.com/science?_ob=MImg&_imagekey=B75H1-4J05Y67-8-1&_cdi=13109&_user=640830&_orig=browse&_coverDate=01%2F14%2F2006&_sk=998549999&view=c&wchp=dGLzVlz-zSkzk&md5=ee9d2a952a112f8b99ffd4cff37e35cd&ie=/sdarticle.pdf"
}