|
|
Refactoring and Verification of the Code of mkfs xfs
Ťulák, Jan ; Peringer, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
This work describes the processes of refactoring mkfs.xfs program for a purpose of refining its code and cleaning the technical debt accumulated over 20 years of the program’s existence. The mkfs.xfs source code is then a subject to static analysis and the used tools (CppCheck, Coverity, Codacy, GCC, Clang) are compared in terms of the number and type of the found defects.
|
|
|
Verifikace programů s ukazateli založená na detekci vzorů
Kubíček, Jan ; Erlebach, Pavel (oponent) ; Vojnar, Tomáš (vedoucí práce)
Tato práce navazuje na výsledky studií v oblasti verifikace nekonečně stavových systémů. Konkrétně se jedná o oblast abstraktního model checkingu. Seznámili jsme se s metodou založenou na abstrakci paměťové konfigurace pomocí paměťových vzorů. Tato metoda byla navržena pro verifikaci programů pracujících s dynamickými paměťovými strukturami jako například seznamy. Na dynamické paměťové struktury je nahlíženo jako na orientované grafy. Verifikace na základě paměťových vzorů abstrahuje obecně libovolné množství vytvořených uzlů do jednoho sumarizovaného uzlu. Tím se dosáhne reprezentace obecně neukončeného grafu konečným zápisem. Poté je možno efektivně provést verifikaci nad tímto abstrahovaným grafem. V naší práci se zabýváme tvorbou modelu pro nástroj implementující verifikaci na základě paměťových vzorů. Model programu je vytvořen z podmnožiny jazyka C. Hlavním přínosem práce je automatizace tvorby modelu pro verifikaci a tím dosáhnutí úplné automatizovanosti procesu verifikace. Je tak možné verifikovat programy napsané v běžném programovacím jazyce. V této práci je diskutována syntaxe vstupního jazyka i implementační detaily překladu.
|
|
|
Efektivní knihovna pro práci s konečnými stromovými automaty
Lengál, Ondřej ; Konečný, Filip (oponent) ; Vojnar, Tomáš (vedoucí práce)
Mnoho současných počítačových systémů používá dynamické datové či řídicí struktury předem neomezené velikosti. Tyto datové struktury mají často charakter stromů nebo se dají zakódovat jako stromy s některými dodatečnými ukazateli nad stromovou kostrou. Této skutečnosti využívají některé v současné době intenzivně studované techniky formální verifikace, které reprezentují nekonečně mnoho stavů konečným stromovým automatem. Nicméně v současnosti neexistuje efektivní a flexibilní implementace knihovny pro stromové automaty, která by byla pro tyto techniky vhodná. Cílem této diplomové práce je takovouto knihovnu poskytnout. Předložený text nejdříve popisuje základy teorie konečných stromových automatů a regulárních stromových jazyků. Dále jsou prozkoumány existující implementace knihoven pro stromové automaty a různé verifikační techniky pro systémy se stromovou strukturou. Poté se text zaobírá návrhem reprezentace stromového automatu a algoritmů provádějících standardní jazykové operace nad touto reprezentací, načež následuje popis implementace knihovny. Prostřednictvím provedených experimentů ukazujeme, že knihovna může konkurovat ostatním dostupným knihovnám pro práci se stromovými automaty, přičemž její výkon v určitých oblastech je řádově vyšší.
|
|
|
Statická detekce častých chyb JBoss aplikačního serveru
Vyvial, Pavel ; Rogalewicz, Adam (oponent) ; Letko, Zdeněk (vedoucí práce)
Práce si klade za úkol poskytnout čtenáři popis statické analýzy prováděné prostřednictvím nástroje FindBugs nad aplikačním serverem JBoss od společnosti Red Hat. Na základě analýzy vybraných chyb byly vytvořeny vzory pro jejich detekci, které byly následně naimplementovány jako zásuvné moduly statického analyzátoru FindBugs (tzv. detektory). Vytvořené detektory byly otestovány na vývojové verzi JBoss aplikačního serveru a výsledky jsou publikovány v závěru práce.
|
|
|
Automata in Decision Procedures and Performance Analysis
Fiedor, Tomáš ; Barnat, Jiří (oponent) ; Radu, Iosif (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis focuses on improving the state of the art of automata-based formal analysis and verification techniques for systems with an infinite state space. In the first part of the thesis, we develop two efficient decision procedures for the WS1S logic, both of them exploiting the correspondence between formulae of WS1S logic and finite automata. We start by proposing a novel antichain-based decision procedure which is, however, limited to formulae in the prenex normal form. Later, we generalize the approach to arbitrary formulae by defining the so-called language terms and constructing an on-the-fly procedure dealing with the terms using lazy techniques. In order to achieve an efficient implementation, we propose numerous optimizations (some of these optimization are not limited to our approaches only). We evaluated both our methods with other recent state-of-the art tools. The achieved results are encouraging and show we can extend the usage of WS1S to wider classes of formulae. The second part of the thesis focuses on resource bounds analysis of heap-manipulating programs. We propose a new class of shape norms based on lengths of paths between distinct points in the heap, which we derive automatically from the analysed program. For this class of norms, we introduce a calculus capable of precisely inferring changes of the analysed norms and use it to generate a corresponding integer representation of an input program followed by dedicated state-of-the art resource bounds analysis. We implemented our approach over the shape analysis based on forest-automata, implemented in the Forester tool, and using a well-established resource bounds analyser, implemented in the Loopus tool. In our experimental evaluation, we show that we indeed obtained a powerful analyser that is able to handle some showcase examples that were never analysed fully automatically before.
|
|
|
Integrace formálních technik do procesu verifikace procesoru RISC-V
Horký, Jakub ; Šnobl, Pavel (oponent) ; Hruška, Tomáš (vedoucí práce)
Tato práce krátce rozebírá architekturu RISC-V a návrh procesorů a jak jednoduše může vzniknout chyba při jejich vytváření. Dále popisuji, jakým způsobem se snaží funkční verifikace tyto chyby odhalit a jaké jsou její výhody a nedostatky. Konkrétněji se zaměřím, jak vypadá verifikační prostředí podle UVM. Popisuji, jakým způsobem do funkční verifikace zapadá formální verifikace a jaké jsou dostupné nástroje pro formální verifikaci. Ke konci této práce popisuji konkrétně způsob mého postupu při psaní tvrzení (psaných v SVA jazyce) pro RISC-V procesor za použití nástroje pro formální verifikaci tvrzení. Při využití těchto tvrzení pro ověření procesoru v pozdější fázi vývoje, kdy funkční verifikace již měla možnost většinu chyb odhalit, se mi přesto podařilo několik chyb najít.
|
|
|
Instrumentace programů pro měření pokrytí při testování SW
Kapoun, Petr ; Peringer, Petr (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato práce se zabývá návrhem a tvorbou instrumentačního nástroje pro měření pokrytí při softwarovém testování. Nástroj při překladu získá reprezentaci vybraných částí programu v podobě grafu toku řízení a instrumentuje dané části programu vložením zpětných volání funkcí. Pomocí dat generovaných při volání vložených funkcí instrumentovaného programu nástroj vyhodnotí měření kritérií pokrytí. Mezi podporovaná kritéria pokrytí patří pokrytí řádků kódu a vybraná kritéria pokrytí toku řízení a toku dat.
|
|
|
Program Loop Unwinding in the 2LS Framework
Nečas, František ; Vojnar, Tomáš (oponent) ; Malík, Viktor (vedoucí práce)
The goal of this work is to propose an improved unwinding mechanism for the 2LS formal verification tool. 2LS is a static analysis framework for C programs based on reasoning about programs using an SMT solver. It combines multiple common verification techniques into an algorithm called k I k I. One of the crucial parts of the algorithm is loop unwinding. Unfortunately, the existing solution does not correctly support unwinding of loops containing operations with dynamically allocated memory. Our proposed solution is based on unwinding loops in a GOTO program rather than the SSA form, making it possible to correctly handle dynamic objects and operations over them. The proposed solution has been implemented in the 2LS framework and our experiments on a set of benchmarks from the International Competition on Software Verification (SV-COMP) show that it improves soundness of analysis of programs working with dynamic objects.
|
|
|
Formal Analysis of Neural Networks
Hudák, David ; Lengál, Ondřej (oponent) ; Češka, Milan (vedoucí práce)
Today, the area where we can use deep learning is becoming broader. It includes safety-critical domains such as traffic or healthcare, and the need for its verification grows. However, sufficient verification toolkits for neural networks, the leading deep learning approach, are still in development. State-of-the-art algorithms now can not verify commonly used deep networks. In this paper, we focus on one of the state-of-the-art solutions, VeriNet. More generally, we focused on the symbolic approach of local robustness analysis. This approach usually relies on creating, processing, and refining the neural network representation, and we focused on the refinement phase. We primarily dealt with the branch and bound algorithm, which in this toolkit splits node inputs in a network to create smaller sub-problems. For this algorithm, we proposed and implemented new split node selection strategies. Specifically, we designed memory-based, alternating, and semi-hierarchical strategies. We achieved significant improvements in the scalability of the VeriNet toolkit. One of our approaches can solve more complex cases and significantly improve already solved cases' performance. Moreover, we discovered an anomaly in the behavior of the verification algorithm we named branch implosions, which led to extreme speed up for some cases. In addition, we extended the set of performed network benchmarks with models from the Marabou package.
|
|
|
Instrumentace C/C++ programů při překladu
Mušková, Kateřina ; Peringer, Petr (oponent) ; Smrčka, Aleš (vedoucí práce)
Tato práce se zabývá návrhem a implementací nástroje TforcTool sloužícího k instrumentaci programů napsaných v jazyce C++, a to instrumentaci přístupu do paměti a volání funkcí. Nástroj staví už na existujícím nástroji Tforc poskytující statickou instrumentaci při překladu, jehož funkcionalitu a použitelnost rozšiřuje. Velkou výhodou oproti stávajícím řešením nabízejícím instrumentaci při překladu je možnost použití nástroje bez změny stávajících překladových skriptů (např. Make).
|
host ::
RSS.