Original title:
Nástroj pro statickou analýzu programů se seznamy
Translated title:
Static Analyzer for List Manipulating Programs
Authors:
Kotoun, Michal ; Lengál, Ondřej (referee) ; Vojnar, Tomáš (advisor) Document type: Bachelor's theses
Year:
2017
Language:
cze Publisher:
Vysoké učení technické v Brně. Fakulta informačních technologií Abstract:
[cze][eng]
Tvorba softwarového analyzátoru je komplexní úloha -- je nutno implementovat parsování zdrojového kódu, reprezentaci instrukcí, abstrakci hodnot, uživatelské rozhraní, ... a také analýzu samu. Abychom předešli zbytečné práci vývojářů analýz, rozhodli jsme se vytvořit framework pro statickou analýzu programů. Předkládáme obecný návrh frameworku zvaného Angie s důrazem na jeho použitelnost a popisujeme prototyp frameworku, včetně modelové analýzy založené na symbolických paměťových grafech. Angie je implementován v C++ a používá nástroje z kolekce LLVM pro parsování zdrojového kódu analyzovaných programů.
Creating a software verification tool is a complex task -- one must implement source code parsing, instruction representation, value abstraction, user interface, ... and the analysis itself. Therefore, we decided to create a static analysis framework to prevent unnecessary wheel reinventing by an analyses implementers. We propose a general design of the framework called Angie with a primary focus on usability, and describe a prototype implementation of the framework, including a model analysis based on symbolic memory graphs. Angie is implemented in C++ and uses the LLVM toolchain as the front-end for parsing the source code of analysed programs.
Keywords:
abstract interpretation; Angie; formal verification; framework; LLVM; Predator; SMG; SSA; static analysis; symbolic memory graphs; abstraktní interpretace; Angie; formální verifikace; framework; LLVM; Predator; SMG; SSA; statická analýza; symbolické paměťové grafy
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/84851