Original title: Statická analýza v prostředí Frama-C zaměřená na detekci uváznutí
Translated title: Static Analysis in the Frama-C Environment Focused on Deadlock Detection
Authors: Dacík, Tomáš ; Holík, Lukáš (referee) ; Vojnar, Tomáš (advisor)
Document type: Bachelor's theses
Year: 2020
Language: eng
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [eng] [cze]
Tato práce se zabývá návrhem nového statického analyzátoru pro detekci uváznutí, implementovaného jako plugin platformy Frama-C. Kromě samotného algoritmu pro detekci uváznutí představuje také odlehčené řešení, které umožňuje využít platformu Frama-C pro analýzu vícevláknových programů s využitím analyzátorů Frama-C podporujících pouze sekvenční programy. Výsledky experimentů ukazují, že implementovaný nástroj je schopný analyzovat reálné programy s vysokou přesností. Pro demonstraci další rozšiřitelnosti je představeno experimentální rozšíření umožňující detekovat také časově závislé chyby nad daty. 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: abstraktní interpretace; analýza vícevláknových programů; Frama-C; statická analýza; uváznutí; časově závislá chyba nad daty; abstract interpretation; analysis of multi-threaded programs; data race; deadlock; Frama-C; static analysis

Institution: Brno University of Technology (web)
Document availability information: Fulltext is available in the Brno University of Technology Digital Library.
Original record: http://hdl.handle.net/11012/191480

Permalink: http://www.nusl.cz/ntk/nusl-416272


The record appears in these collections:
Universities and colleges > Public universities > Brno University of Technology
Academic theses (ETDs) > Bachelor's theses