Detail práce
Verifikace ukazatelových programů pomocí lesních automatů
V této práci je rozvíjena existující metoda pro shape analýzu programů založená na lesních automatech. Dále je také vylepšována implementace této metody, nástroj Forester. Lesní automaty jsou založeny na stromových automatech, jejichž jednoduchou implementaci Forester obsahuje. Prvním přínosem této práce je nahrazení této implementace knihovnou VATA, která obsahuje efektivní algoritmy pro reprezentaci a manipulaci stromových automatů. Verze nástroje Forester používající knihovnu VATA se zúčastnila mezinárodní soutěže SV-COMP 2015. Dále je verifikace založená na lesních automatech v této práci rozšířena o predikátovou abstrakci a analýzu nalezených protipříkladů. Výsledek této analýzy je možné využít následujícími způsoby. Prvním je určení toho, zda je nalezené chyba reálná nebo naopak nepravá. Druhým je pak zjemnění predikátové abstrakce pomocí predikátů odvozených při zpětném běhu. Obě techniky byly také implementovány v nástroji Forester. Na závěr je zhodnoceno zlepšení, které tyto techniky přinesly oproti původní verzi nástroje Forester.
lesní automaty, formální verifikace, statická analýza, složité datové struktury, stromové automaty, zpětný běh, predikátová abstrakce.
Student nejprve prezentoval výsledky, kterých dosáhl v rámci své práce. Komise se poté seznámila s hodnocením vedoucího a posudkem oponenta práce. Student následně odpověděl na otázky oponenta a na další otázky přítomných. Komise se na základě posudku oponenta, hodnocení vedoucího, přednesené prezentace a odpovědí studenta na položené otázky rozhodla práci hodnotit stupněm "A"
- Jak složité by bylo dodělat možnost použití hierarchických FA v rámci predikátové abstrakce?
Burget Radek, doc. Ing., Ph.D. (UIFS FIT VUT), člen
Drahanský Martin, prof. Ing., Dipl.-Ing., Ph.D. (UITS FIT VUT), člen
Hrubý Martin, Ing., Ph.D. (UITS FIT VUT), člen
Rozinajová Viera, doc. Ing., Ph.D. (FIIT STU), člen
Ryšavý Ondřej, doc. Ing., Ph.D. (UIFS FIT VUT), člen
@mastersthesis{FITMT17838,
author = "Martin Hru\v{s}ka",
type = "Diplomov\'{a} pr\'{a}ce",
title = "Verifikace ukazatelov\'{y}ch program\r{u} pomoc\'{i} lesn\'{i}ch automat\r{u}",
school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
year = 2015,
location = "Brno, CZ",
language = "czech",
url = "https://www.fit.vut.cz/study/thesis/17838/"
}