|
|
Static Analysis of C Programs in Sparse and Similar Tools
Nagy, Martin ; Peringer, Petr (referee) ; Vojnar, Tomáš (advisor)
Software verification is steadily becoming important for software developers and companies to ensure software quality. However, the problem of writing a good static code analysis tool often stems from the lack of a good compiler front-end. To solve this problem, we try to analyse and document an existing tool called Sparse to empower software verification researchers with a ready, stable solution for their projects. Additionally, we also talk about Mygcc and it's new approach to integrate with existing compilers.
|
|
|
An Extension of the ANaConDa Tool for Dynamic Analysis of Concurrent Programs
Horňák, Michal ; Češka, Milan (referee) ; Vojnar, Tomáš (advisor)
The main goal of this thesis is to implement algorithm FastTrack for dynamic analysis of multi-threaded programs in C/C++. FastTrack is algorithm which detects data race errors. It is based on happens-before relation encoded into the vector-clocks.Vector-clocks allows extrapolation of the execution which improves detection of potential errors, which were not seen in the actual run of the program however in other executions they could cause problems. Algorithm is implemented into the framework ANaConDA. ANaConDA is a tool for implementation of dynamic analyzers of parallel programs on binary level. It provides neccessary run time program informations for detectors use to discover concurency errors.
|
|
|
Comparing Languages and Reducing Automata Used in Network Traffic Filtering
Havlena, Vojtěch ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
The focus of this thesis is the comparison of languages and the reduction of automata used in network traffic monitoring. In this work, several approaches for approximate (language non-preserving) reduction of automata and comparison of their languages are proposed. The reductions are based on either under-approximating the languages of automata by pruning their states, or over-approximating the language by introducing new self-loops (and pruning redundant states later). The proposed approximate reduction methods and the proposed probabilistic distance utilize information from a network traffic. Formal guarantees with respect to a model of network traffic, represented using a probabilistic automaton are provided. The methods were implemented and evaluated on automata used in network traffic filtering.
|
|
|
Coverability for Parallel Programs
Turoňová, Lenka ; Vojnar, Tomáš (referee) ; Holík, Lukáš (advisor)
This work is focusing on automatic verification of systems with parallel running processes. We discuss the existing methods and certain possibilities of optimizing them. Existing techniques are essentially based on finding an inductive invariant (for instance using a variant of counterexample-guided abstract refinement (CEGAR)). The effectiveness of these methods depends on the size of the invariant. In this thesis, we explored the possibility of improving the methods by focusing on finding invariants of minimal size. We implemented a tool that facilitates exploring the space of invariants of the system under scrutiny. Our experimental results show that many practical existing systems indeed have invariants that are much smaller than what can be found by the existing methods. The conjectures and the results of the work will serve as a basis of future research of an efficient method for finding small invariants of parallel systems.
|
|
|
Simulace a protiřetězce pro efektivní práci s konečnými automaty
Holík, Lukáš ; Černá, Ivana (referee) ; Jančar, Petr (referee) ; Vojnar, Tomáš (advisor)
Cílem této práce je vývoj technik umožňujících praktické využití nedeterministických konečných automatů, zejména nedeterministických stromových automatů. Jde zvláště o techniky pro redukci velikosti a testování jazykové inkluze, jež hrají zásadní roli v mnoha oblastech aplikace konečných automatů. V oblasti redukce velikosti vycházíme z dobře známých metod pro slovní automaty které jsou založeny na relacích simulace. Navrhli jsme efektivní algoritmy pro výpočet stromových variant simulačních relací a identifikovali jsme nový typ relace založený na kombinaci takzvaných horních a dolních simulací nad stromovými automaty. Tyto kombinované relace jsou zvláště vhodné pro redukci velikosti automatů slučováním stavů. Navržený princip kombinace relací simulace je relevantní i pro slovní automaty. Náš přínos v oblasti testování jazykové inkluze je dvojí. Nejprve jsme zobecnili na stromové automaty takzvané protiřetězcové algoritmy, které byly původně navrženy pro slovními automaty. Dále se nám podařilo použitím simulačních relací výrazně zefektivnit protiřetězcové algoritmy pro testování jazykové inkluze jak pro slovní, tak pro stromové automaty. Relevanci našich technik pro praxi jsme demonstrovali jejich nasazením v rámci regulárního stromového model checkingu, což je verifikační metoda založená na stromových automatech. Použití našich algoritmů zde vedlo k výraznému zrychlení a zvětšení škálovatelnosti celé metody. Základní myšlenky našich algoritmů pro redukci velikosti automatů a testování jazykové inkluze jsou aplikovatelné i na jiné typy automatů. Příkladem jsou naše redukční techniky pro alternující Büchiho automaty prezentované v poslední části práce.
|
|
|
An Extension of the ANaConDa Tool for Dynamic Analysis of Concurrent Programs
Horňák, Michal ; Křena, Bohuslav (referee) ; Vojnar, Tomáš (advisor)
The main goal of this thesis is to implement algorithm FastTrack for dynamic analysis of multi-threaded programs in C/C++. FastTrack is algorithm which detects data race errors. It is based on happens-before relation encoded into the vector-clocks. Vector-clocks allows extrapolation of the execution which improves detection of potential errors, which were not seen in the actual run of the program however in other executions they could cause problems. Algorithm is implemented into the framework ANaConDA. ANaConDA is a tool for implementation of dynamic analyzers of parallel programs on binary level. It provides neccessary run time program informations for detectors use to discover concurency errors.
|
|
|
Static Analysis Using Facebook Infer Focused on Deadlock Detection
Marcin, Vladimír ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
Static analysis has nowadays become one of the most popular ways of catching bugs early in the modern software. However, a frequent problem of static analysers, which are reasonably precise, is their scalability. Moreover, these which are efficient and scale (e.g.: Coverity, KlockWork, etc.) are often proprietary and difficult to openly evaluate or extend. An improvement to this state of practice is brought Facebook Infer, which offers an open-source framework for compositional and incremental static analysis. In this thesis, we present our Low-Level Deadlock Detector (L2D2) extending the capabilities of Infer. Our algorithm fits the compositional analysis, based on a context independent computation of a summary for each function, which results in its high scalability. We have implemented the algorithm and evaluated it on a benchmark consisting of real-life programs derived from the Debian GNU/Linux with in total 11.4 MLOC. While neither sound nor complete, our approach is effective in practice, finding all known deadlocks and giving false alarms in less than 4% of the considered programs only.
|
|
|
Visualising CPU Activity
Ďurčo, Marián ; Češka, Milan (referee) ; Vojnar, Tomáš (advisor)
This thesis is intended to be a complement for learning about the RISC pipeline. Product of this thesis is a web application. After reviewing various tools and libraries suitable for this work, we have chosen two main libraries React and Redux. The created solution allows the instruction flow to be displayed in the RISC pipeline as well as states of the registers and the memory. It makes easy to perform transitions between the various parts of the visualization. This visualization allows a basic understanding of the RISC pipeline principles and also individual assembly instructions.
|
|
|
Reductions of Automata Used in Network Traffic Filtering
Semrič, Jakub ; Hruška, Martin (referee) ; Vojnar, Tomáš (advisor)
The aim of this work is to propose scalable methods for reducing non-deterministic finite automata used in network traffic filtering. We introduce two approaches of NFAs reduction based on states elimination. To achieve a substantial reduction of automata, we use language non-preserving techniques with a primary focus on language over-approximation, since language preserving methods may not provide sufficient reduction. We implemented the methods and evaluated the accuracy of the reduced automata on real traffic. Our approach does not provide any formal guarantee wrt unseen input traffic, but on the other hand, it can be smoothly used on automata of any size, which is a significant problem for existing methods that have very high time complexity and cannot be applied on really large automata.
|
|
|
Improved Tools for Handling deltarpm Files
Chalk, Matěj ; Hruška, Martin (referee) ; Vojnar, Tomáš (advisor)
Na platformě Fedora se používají balíčky RPM pro instalaci softwaru. Každá verze takto distribuovaného softwaru odpovídá samostatnému souboru RPM. Aktualizace softwaru pak odpovídá stáhnutí velkého souboru RPM, který je ve skutečnosti velmi podobný již nainstalovnému balíčku. Balíčky DeltaRPM poskytují alternativu pro aktualizaci softwaru. Jedná se o speciální patch soubory, které uchovávají rozdíl mezi dvěma soubory RPM. Aktualizace pak spočívá ve stáhnutí daleko menšího souboru a aplikaci tohoto patche na starší verzi příslušného RPM. Projekt deltarpm definuje formát souborů DeltaRPM a nabízí nástroje pro příkazovou řádku, které realizují jejich vytváření a aplikaci. Tato implementace je však nevhodná pro použití jako knihovna. Cíl této práce je vytvořit novou implementaci nástrojů pro vytváření a aplikaci souborů DeltaRPM, která je zpětně kompatibilní a poskytuje knihovnu pro vývojáře v jazyce C, která vyřeší některé slabiny současné implementace.
|
guest ::
