Název: Integrace nástrojů Predator a Symbiotic pro analýzu software
Překlad názvu: Integration of the Predator and Symbiotic Software Analysers
Autoři: Kinšt, Ondřej ; Malík, Viktor (oponent) ; Vojnar, Tomáš (vedoucí práce)
Typ dokumentu: Diplomové práce
Rok: 2024
Jazyk: eng
Nakladatel: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstrakt: [eng] [cze]
Tato diplomová práce zkoumá integraci dvou významných nástrojů pro analýzu softwaru, Predator a Symbiotic, které se využívají k detekci chyb paměťové bezpečnosti (memory-safety errors) v programech v jazyce C. Výzkum se zaměřuje na zdokonalení stávající integrace těchto nástrojů využitím symbolických paměťových grafů (SMG) nástroje Predator, aby byla zajištěna přesnější analýza přiřazení ukazatelů (points-to analysis) pro knihovnu DG používanou nástrojem Symbiotic. Navrhovaná metoda zahrnuje transformaci SMG do grafů přiřazení ukazatelů (points-to graphs), což umožňuje přesnější analýzu vztahů mezi ukazateli a paměťovými lokacemi. Práce popisuje návrh a implementaci této integrace, včetně vývoje nových algoritmů a úprav stávajících nástrojů. Výsledky experimentálních vyhodnocení na benchmarkových testech ze soutěže SV-COMP a dalších testovacích sadách jsou uvedeny. This thesis explores the integration of two prominent software analysis tools, Predator and Symbiotic, which are utilised for detecting memory-safety errors in C programs. The research focuses on enhancing the existing integration of these tools by leveraging Predator’s symbolic memory graphs (SMGs) to provide a more precise points-to analysis for the DG library used by Symbiotic. The proposed method involves transforming SMGs into points-to graphs, enabling more accurate analysis of pointer relationships and memory locations. The thesis details the design and implementation of this integration, including the development of new algorithms and modifications to the existing tools. Results of experimental evaluations on benchmarks from the SV-COMP competition and other testing suites are provided.
Klíčová slova: C; DG library; points-to analysis; Predator; program verification; software analysis tools; static analysis; Symbiotic; C; knihovna DG; nástroje pro analýzu softwaru; points-to analýza; Predator; statická analýza; Symbiotic; verifikace programů

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: https://hdl.handle.net/11012/249603

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


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 > Diplomové práce