Original title: Integrace nástrojů Predator a Symbiotic pro analýzu software
Translated title: Integration of the Predator and Symbiotic Software Analysers
Authors: Kinšt, Ondřej ; Malík, Viktor (referee) ; Vojnar, Tomáš (advisor)
Document type: Master’s theses
Year: 2024
Language: eng
Publisher: Vysoké učení technické v Brně. Fakulta informačních technologií
Abstract: [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.
Keywords: C; knihovna DG; nástroje pro analýzu softwaru; points-to analýza; Predator; statická analýza; Symbiotic; verifikace programů; C; DG library; points-to analysis; Predator; program verification; software analysis tools; static analysis; Symbiotic

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

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


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