Detail publikace
Verification of Programs with Complex Data Structures
Formální verifikace, model checking, nekonečně stavové systémy, regulární stromové jazyky, automatická abstrakce, verifikace programů s rekurzivními dynamickými datovými strukturami, verifikace konečnosti běhu programů.
V této práci se věnujeme metodám verifikace nekonečně stavových systémů, konkrétněmetodám založených na principu regulární stromový model checking. Jako první částnašeho vlastního přínosu uvádíme obecnou metodu pro verifikace nekonečně stavovýchsystémů-abstraktní regulární stromový model checking (ARTMC). Metoda je kombinacíregulárního stromového model checkingu s automatickou abstrakcí. Dále pak prezentujemenaši originální metodu pro verifikaci programů pracujících s dynamickými datovýmistrukturami. Metoda je založená na ARTMC a s její pomocí byla zverifikována řada procedurpracujících s ukazateli. Některé z těchto procedur byly vůbec poprvé zverifikoványplně automaticky. Jako poslední část našeho vlastního přínosu uvádíme metodu určenoupro verifikace konečnosti běhu programů pracujících se stromovými datovými strukturami.Metoda je založená na kombinaci ARTMC a čítačových automatů a byla úspěšněapliková na na několik procedur pracujících se stromy.
@book{BUT61788,
author="Adam {Rogalewicz}",
title="Verification of Programs with Complex Data Structures",
year="2007",
address="Brno",
pages="122",
isbn="978-80-214-3548-3",
url="http://www.fit.vutbr.cz/%7Erogalew/pubs/rogalewicz-PhD-thesis.pdf"
}