Thesis Details

Static Analysis in the Frama-C Environment Focused on Deadlock Detection

Bachelor's Thesis Student: Dacík Tomáš Academic Year: 2019/2020 Supervisor: Vojnar Tomáš, prof. Ing., Ph.D.
Czech title
Statická analýza v prostředí Frama-C zaměřená na detekci uváznutí
Language
English
Abstract

This thesis presents a design of a new static analyser focused on deadlock detection, implemented as a plugin of the Frama-C platform. Together with the core algorithm of deadlock detection, we also present a light-weight method that allows one to analyse (not only for the purposes of deadlock detection) multi-threaded programs using sequential analysers of Frama-C. Results of experiments show that our tool is able to handle real-world C code with high precision. Moreover, we demonstrate its extensibility by so-far experimental implementation of data race detection.

Keywords

deadlock, data race, static analysis, abstract interpretation, analysis of multi-threaded programs, Frama-C

Department
Department of Intelligent Systems FIT BUT
Degree Programme
Information Technology
Files
Status
defended, grade A
Date
10 July 2020
Reviewer
Holík Lukáš, doc. Mgr., Ph.D.
Committee
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT), předseda
Kekely Lukáš, Ing., Ph.D. (DCSY FIT BUT), člen
Křivka Zbyněk, Ing., Ph.D. (DIFS FIT BUT), člen
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS FIT BUT), člen
Španěl Michal, Ing., Ph.D. (DCGM FIT BUT), člen
Citation
DACÍK, Tomáš. Static Analysis in the Frama-C Environment Focused on Deadlock Detection. Brno, 2020. Bachelor's Thesis. Brno University of Technology, Faculty of Information Technology. 2020-07-10. Supervised by Vojnar Tomáš. Available from: https://www.fit.vut.cz/study/thesis/22928/
BibTeX 
@bachelorsthesis{FITBT22928,
    author = "Tom\'{a}\v{s} Dac\'{i}k",
    type = "Bachelor's thesis",
    title = "Static Analysis in the Frama-C Environment Focused on Deadlock Detection",
    school = "Brno University of Technology, Faculty of Information Technology",
    year = 2020,
    location = "Brno, CZ",
    language = "english",
    url = "https://www.fit.vut.cz/study/thesis/22928/"
}

Theses

Back to top