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