Thesis Details

Statická analýza v nástroji Facebook Infer zaměřená na detekci porušení atomičnosti

Bachelor's Thesis Student: Harmim Dominik Academic Year: 2018/2019 Supervisor: Vojnar Tomáš, prof. Ing., Ph.D.
English title
Static Analysis Using Facebook Infer to Find Atomicity Violations
Language
Czech
Abstract

The goal of this thesis is to propose a static analyser that detects atomicity violations. The proposed analyser Atomer is implemented as a module of Facebook Infer, which is an open-source and extendable static analysis framework that promotes efficient modular and incremental analysis. The analyser works on the level of sequences of function calls. The proposed solution is based on the assumption that sequences executed atomically once should probably be executed always atomically. The implemented analyser has been successfully verified and evaluated on both smaller programs created for testing purposes as well as publicly available benchmarks derived from real-life low-level programs.

Keywords

static analysis, programs analysis, abstract interpretation, Facebook Infer, atomicity violation, concurrent programs, contracts for concurrency, atomic sequences, atomicity, incremental analysis, modular analysis, compositional analysis, interprocedural analysis

Department
Degree Programme
Information Technology
Files
Status
defended, grade A
Date
10 June 2019
Reviewer
Committee
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT), předseda
Grézl František, Ing., Ph.D. (DCGM FIT BUT), člen
Honzík Jan M., prof. Ing., CSc. (DIFS FIT BUT), člen
Kořenek Jan, doc. Ing., Ph.D. (DCSY FIT BUT), člen
Smrčka Aleš, Ing., Ph.D. (DITS FIT BUT), člen
Citation
HARMIM, Dominik. Statická analýza v nástroji Facebook Infer zaměřená na detekci porušení atomičnosti. Brno, 2019. Bachelor's Thesis. Brno University of Technology, Faculty of Information Technology. 2019-06-10. Supervised by Vojnar Tomáš. Available from: https://www.fit.vut.cz/study/thesis/21689/
BibTeX
@bachelorsthesis{FITBT21689,
    author = "Dominik Harmim",
    type = "Bachelor's thesis",
    title = "Statick\'{a} anal\'{y}za v n\'{a}stroji Facebook Infer zam\v{e}\v{r}en\'{a} na detekci poru\v{s}en\'{i} atomi\v{c}nosti",
    school = "Brno University of Technology, Faculty of Information Technology",
    year = 2019,
    location = "Brno, CZ",
    language = "czech",
    url = "https://www.fit.vut.cz/study/thesis/21689/"
}
Back to top