Detail publikace

Verification of Programs with Complex Data Structures

ROGALEWICZ Adam. Verification of Programs with Complex Data Structures. Brno, 2007. ISBN 978-80-214-3548-3.
Název česky
Verifikace programů se složitými datovými strukturami
Typ
kniha
Jazyk
angličtina
Autoři
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT)
URL
Klíčová slova

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ů.

Abstrakt

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í část našeho vlastního přínosu uvádíme obecnou metodu pro verifikace nekonečně stavových systémů-abstraktní regulární stromový model checking (ARTMC). Metoda je kombinací regulárního stromového model checkingu s automatickou abstrakcí. Dále pak prezentujeme naši originální metodu pro verifikaci programů pracujících s dynamickými datovými strukturami. Metoda je založená na ARTMC a s její pomocí byla zverifikována řada procedur pracujících s ukazateli. Některé z těchto procedur byly vůbec poprvé zverifikovány plně automaticky. Jako poslední část našeho vlastního přínosu uvádíme metodu určenou pro 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.

Rok
2007
Strany
122
ISBN
978-80-214-3548-3
Místo
Brno, CZ
BibTeX 
@BOOK{FITPUB8522,
   author = "Adam Rogalewicz",
   title = "Verification of Programs with Complex Data Structures",
   pages = 122,
   year = 2007,
   location = "Brno, CZ",
   ISBN = "978-80-214-3548-3",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/8522"
}
Nahoru