Thesis Details
Statická analýza v nástroji Facebook Infer zaměřená na detekci uváznutí
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.
static analysis, abstract interpretation, Facebook Infer, deadlock detection, Infer.AI framework, L2D2
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
@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/" }