Název: Statická analýza v prostředí Frama-C zaměřená na detekci uváznutí
Překlad názvu: Static Analysis in the Frama-C Environment Focused on Deadlock Detection
Autoři: Dacík, Tomáš ; Holík, Lukáš (oponent) ; Vojnar, Tomáš (vedoucí práce)
Typ dokumentu: Bakalářské práce
Rok: 2020
Jazyk: eng
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [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.
Klíčová slova: abstract interpretation; analysis of multi-threaded programs; data race; deadlock; Frama-C; static analysis; abstraktní interpretace; analýza vícevláknových programů; Frama-C; statická analýza; uváznutí; časově závislá chyba nad daty

Instituce: Vysoké učení technické v Brně (web)
Informace o dostupnosti dokumentu: Plný text je dostupný v Digitální knihovně VUT.
Původní záznam: http://hdl.handle.net/11012/191480

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-416272


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Vysoké učení technické v Brně
Vysokoškolské kvalifikační práce > Bakalářské práce