Thesis Details

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

Bachelor's Thesis Student: Kotoun Michal Academic Year: 2016/2017 Supervisor: Vojnar Tomáš, prof. Ing., Ph.D.
English title
Static Analyzer for List Manipulating Programs
Language
Czech
Abstract

Creating a software verification tool is a complex task -- one must implement source code parsing, instruction representation, value abstraction, user interface, ... and the analysis itself. Therefore, we decided to create a static analysis framework to prevent unnecessary wheel reinventing by an analyses implementers. We propose a general design of the framework called Angie with a primary focus on usability, and describe a prototype implementation of the framework, including a model analysis based on symbolic memory graphs. Angie is implemented in C++ and uses the LLVM toolchain as the front-end for parsing the source code of analysed programs.

Keywords

static analysis, abstract interpretation, formal verification, LLVM, SSA, Predator, SMG, symbolic memory graphs, framework, Angie

Department
Degree Programme
Files
Status
defended
Date
29 August 2017
Reviewer
Committee
Růžička Richard, doc. Ing., Ph.D., MBA (DCSY FIT BUT), předseda
Hliněná Dana, doc. RNDr., Ph.D. (DMAT FEEC BUT), člen
Chudý Peter, doc. Ing., Ph.D. MBA (DCGM FIT BUT), člen
Kreslíková Jitka, doc. RNDr., CSc. (DIFS FIT BUT), člen
Křena Bohuslav, Ing., Ph.D. (DITS FIT BUT), člen
Citation
KOTOUN, Michal. Nástroj pro statickou analýzu programů se seznamy. Brno, 2017. Bachelor's Thesis. Brno University of Technology, Faculty of Information Technology. 2017-08-29. Supervised by Vojnar Tomáš. Available from: https://www.fit.vut.cz/study/thesis/19905/
BibTeX
@bachelorsthesis{FITBT19905,
    author = "Michal Kotoun",
    type = "Bachelor's thesis",
    title = "N\'{a}stroj pro statickou anal\'{y}zu program\r{u} se seznamy",
    school = "Brno University of Technology, Faculty of Information Technology",
    year = 2017,
    location = "Brno, CZ",
    language = "czech",
    url = "https://www.fit.vut.cz/study/thesis/19905/"
}
Back to top