Detail práce

Nástroj pro statickou analýzu programů se seznamy

Bakalářská práce Student: Kotoun Michal Akademický rok: 2016/2017 Vedoucí: Vojnar Tomáš, prof. Ing., Ph.D.
Název anglicky
Static Analyzer for List Manipulating Programs
Jazyk práce
český
Abstrakt

Tvorba softwarového analyzátoru je komplexní úloha -- je nutno implementovat parsování zdrojového kódu, reprezentaci instrukcí, abstrakci hodnot, uživatelské rozhraní, ... a také analýzu samu. Abychom předešli zbytečné práci vývojářů analýz, rozhodli jsme se vytvořit framework pro statickou analýzu programů. Předkládáme obecný návrh frameworku zvaného Angie s důrazem na jeho použitelnost a popisujeme prototyp frameworku, včetně modelové analýzy založené na symbolických paměťových grafech. Angie je implementován v C++ a používá nástroje z kolekce LLVM pro parsování zdrojového kódu analyzovaných programů.

Klíčová slova

statická analýza, abstraktní interpretace, formální verifikace, LLVM, SSA, Predator, SMG, symbolické paměťové grafy, framework, Angie

Ústav
Ústav inteligentních systémů FIT VUT v Brně
Studijní program
Soubory
Stav
obhájeno
Obhajoba
29. srpna 2017
Oponent
Lengál Ondřej, Ing., Ph.D.
Průběh obhajoby

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

Otázky u obhajoby

Jak je složité rozšířit rámec o novou analýzu? Co vše je pro to potřeba provést a jaká je očekávaná časová náročnost pro vývojáře analýzy?

  1. Jaké jsou výhody použití rámce oproti např. přímému použití LLVM mezikódu?
Komise
Růžička Richard, doc. Ing., Ph.D., MBA (UPSY FIT VUT), předseda
Hliněná Dana, doc. RNDr., Ph.D. (UMAT FEKT VUT), člen
Chudý Peter, doc. Ing., Ph.D. MBA (UPGM FIT VUT), člen
Kreslíková Jitka, doc. RNDr., CSc. (UIFS FIT VUT), člen
Křena Bohuslav, Ing., Ph.D. (UITS FIT VUT), člen
Citace
KOTOUN, Michal. Nástroj pro statickou analýzu programů se seznamy. Brno, 2017. Bakalářská práce. Vysoké učení technické v Brně, Fakulta informačních technologií. 2017-08-29. Vedoucí práce Vojnar Tomáš. Dostupné z: https://www.fit.vut.cz/study/thesis/19905/
BibTeX 
@bachelorsthesis{FITBT19905,
    author = "Michal Kotoun",
    type = "Bakal\'{a}\v{r}sk\'{a} pr\'{a}ce",
    title = "N\'{a}stroj pro statickou anal\'{y}zu program\r{u} se seznamy",
    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 = "czech",
    url = "https://www.fit.vut.cz/study/thesis/19905/"
}

Závěrečné práce

Nahoru