Detail práce
Template-Based Synthesis of Heap Abstractions
Cieľom tejto práce je návrh analýzy tvaru haldy vhodnej pre potreby analyzátora 2LS. 2LS je nástroj pre analýzu C programov založený na automatickom odvodzovaní invariantov s použitím SMT solvera. Navrhované riešenie obsahuje spôsob reprezentácie tvaru programovej haldy pomocou logických formulí nad teóriou bitových vektorov. Tie sú následne využité v SMT solveri pre predikátovú logiku prvého rádu na odvodenie invariantov cyklov a súhrnov jednotlivých funkcií analyzovaného programu. Náš prístup je založený na ukazateľových prístupových cestách, ktoré vyjadrujú dosiahnuteľnosť objektov na halde z ukazateľových premenných. Informácie získané z analýzy môžu byť využité na dokázanie rôznych vlastností programu súvisiacich s prácou s dynamickýcmi dátovými štruktúrami. Riešenie bolo implementované v rámci nástroja 2LS. S jeho použitím došlo k výraznému zlepšeniu schopnosti 2LS analyzovať programy pracujúce s ukazateľmi a dynamickými dátovými štruktúrami. Toto je demonštrované na sade experimentov prevzatých zo známej medzinárodnej súťaže vo verifikácii programov SV-COMP a iných experimentoch.
formálna verifikácia, analýza programov, 2LS, analýza založená na šablónach, analýza tvaru haldy, zreťazené zoznamy, prístupové cesty na halde, abstraktná interpretácia, SSA forma, odvodzovanie invariantov, súhrny funkcií, dynamické dátové štruktúry
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 - výborně.
- Uvažoval jste, jak obtížné bude rozšířit navržený přístup na stromové struktury?
Čadík Martin, doc. Ing., Ph.D. (UPGM FIT VUT), člen
Češka Milan, doc. RNDr., Ph.D. (UITS FIT VUT), člen
Janoušek Jan, doc. Ing., Ph.D. (FIT ČVUT), člen
Orság Filip, Ing., Ph.D. (UITS FIT VUT), člen
Zachariášová Marcela, Ing., Ph.D. (UPSY FIT VUT), člen
@mastersthesis{FITMT19901,
author = "Viktor Mal\'{i}k",
type = "Diplomov\'{a} pr\'{a}ce",
title = "Template-Based Synthesis of Heap Abstractions",
school = "Vysok\'{e} u\v{c}en\'{i} technick\'{e} v Brn\v{e}, Fakulta informa\v{c}n\'{i}ch technologi\'{i}",
year = 2017,
location = "Brno, CZ",
language = "english",
url = "https://www.fit.vut.cz/study/thesis/19901/"
}