Thesis Details

Statická analýza v nástroji Facebook Infer zaměřená na detekci uváznutí

Bachelor's Thesis Student: Marcin Vladimír Academic Year: 2018/2019 Supervisor: Vojnar Tomáš, prof. Ing., Ph.D.
English title
Static Analysis Using Facebook Infer Focused on Deadlock Detection
Language
Czech
Abstract

Static analysis has nowadays become one of the most popular ways of catching bugs early in the modern software. However, a frequent problem of static analysers, which are reasonably precise, is their scalability. Moreover, these which are efficient and scale (e.g.: Coverity, KlockWork, etc.) are often proprietary and difficult to openly evaluate or extend. An improvement to this state of practice is brought Facebook Infer, which offers an open-source framework for compositional and incremental static analysis. In this thesis, we present our Low-Level Deadlock Detector (L2D2) extending the capabilities of Infer. Our algorithm fits the compositional analysis, based on a context independent computation of a summary for each function, which results in its high scalability. We have implemented the algorithm and evaluated it on a benchmark consisting of real-life programs derived from the Debian GNU/Linux with in total 11.4 MLOC. While neither sound nor complete, our approach is effective in practice, finding all known deadlocks and giving false alarms in less than 4% of the considered programs only.

Keywords

static analysis, abstract interpretation, Facebook Infer, deadlock detection, Infer.AI framework, L2D2

Department
Department of Intelligent Systems FIT BUT
Degree Programme
Information Technology
Files
Status
defended, grade A
Date
10 June 2019
Reviewer
Rogalewicz Adam, doc. Mgr., Ph.D.
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
MARCIN, Vladimír. Statická analýza v nástroji Facebook Infer zaměřená na detekci uváznutí. 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/21920/
BibTeX 
@bachelorsthesis{FITBT21920,
    author = "Vladim\'{i}r Marcin",
    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 uv\'{a}znut\'{i}",
    school = "Brno University of Technology, Faculty of Information Technology",
    year = 2019,
    location = "Brno, CZ",
    language = "czech",
    url = "https://www.fit.vut.cz/study/thesis/21920/"
}

Theses

Back to top