|
|
Analýza práce s dynamickými datovými strukturami v C programech
Šoková, Veronika ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
Táto diplomová práca sa zaoberá analýzou dynamických dátových štruktúr pomocou analýzy tvaru použitej v nástroji Predator. Popisuje zvolenú abstraktnú doménu pre reprezentáciu pamäte vo forme symbolických grafov pamäte. Ďalej sa zaoberá návrhom prostredia pre vývoj statických analyzátorov nad clang/LLVM. Prínosom tejto práce je vytvorenie a otestovanie transformačných priechodov zjednodušujúcich LLVM IR medzikód. Ďalším prínosom je optimalizácia parametrov paralelnej nadstavby Predatora opakovaným spúšťaním testov z medzinárodnej súťaže SV-COMP'16, kde táto verzia nástroja Predator získala zlatú medailu v kategórii Heap Data Structures. Posledným prínosom je návrh architektúry samotného verifikačného jadra s ohľadom na SMG doménu.
|
|
|
Automata in Infinite-state Formal Verification
Lengál, Ondřej ; Jančar, Petr (oponent) ; Veith, Helmut (oponent) ; Esparza, Javier (oponent) ; Vojnar, Tomáš (vedoucí práce)
The work presented in this thesis focuses on finite state automata over finite words and finite trees, and the use of such automata in formal verification of infinite-state systems. First, we focus on extensions of a previously introduced framework for verifi cation of heap-manipulating programs-in particular programs with complex dynamic data structures-based on tree automata. We propose several extensions to the framework, such as making it fully automated or extending it to consider ordering over data values. Further, we also propose novel decision procedures for two logics that are often used in formal verification: separation logic and weak monadic second order logic of one successor. These decision procedures are based on a translation of the problem into the domain of automata and subsequent manipulation in the target domain. Finally, we have also developed new approaches for efficient manipulation with tree automata, mainly for testing language inclusion and for handling automata with large alphabets, and implemented them in a library for general use. The developed algorithms are used as the key technology to make the above mentioned techniques feasible in practice.
|
|
|
Analýza časového vývoje léčených nádorů páteře v CT datech
Nohel, Michal ; Jan, Jiří (oponent) ; Jakubíček, Roman (vedoucí práce)
Tato diplomová práce se zabývá časovým vývojem léčených nádorů páteře v CT datech. V teoretické části se zabývá anatomií, fyziologií a patofyziologií páteře a těl obratlů. Dále popisuje diagnostické a terapeutické možnosti detekce a léčby nádorů páteře. Její součástí je přehled současného stavu využití časové analýzy v onkologii. Jsou diskutovány problémy dostupných anotací a jsou vytvořeny nové databáze pro následnou analýzu. Dále je navržena metodologie časové analýzy podle tvarové charakterizace a velikosti postižení obratle. Na vytvořené databáze jsou aplikovány navržené metodické přístupy extrakce příznaků. Jejich volba a vhodnost je diskutována, včetně jejich potenciálu pro případné využití pro klinickou praxi sledování vývoje a odvozování charakteristických závislostí příznaků na prognóze pacienta.
|
|
|
Creation of Database and Classification of Diatoms
Svoboda, Jan ; Nötzel, Ralf (oponent) ; Drahanský, Martin (vedoucí práce)
The final application works with the designed database, containing images of the individual diatoms and the information about them stored in XML file. The basic operations over this database are secured, such as adding, modification, deleting and searching. The searching can be performed in three ways, by means of textual inputs, image inputs or their combination. The algorithm of searching by means of image inputs tries to find the most similar candidates within the database, considering the shape and thickness of a diatom shell and the internal structure of a diatom itself. This search is specified mostly by the quality of obtained pictures or images of the diatoms compared. The program contains a clear and intuitive graphic interface that conveniently enables us to browse the current database and to perform operations over it, contains set up filters for better recognition.
|
|
|
Template-Based Synthesis of Heap Abstractions
Malík, Viktor ; Hruška, Martin (oponent) ; Vojnar, Tomáš (vedoucí práce)
The goal of this work is to propose a shape analysis suitable for the context of the 2LS analyser. 2LS is a program analysis framework for C programs which is based on automatic invariant inference using an SMT solver. The proposed solution includes a way how the shape of a program heap can be described using logical formulae over bit-vectors and how a first-order SMT solver can be used to infer loop invariants and function summaries for each function of the analysed program. Our approach is based on pointer access paths that describe the shape of the heap by expressing the reachability of heap objects from pointer-typed program variables. The information obtained from the analysis can be used to prove various properties of programs manipulating dynamic data structures, mainly linked lists. The solution has been implemented in the 2LS framework and it brought a significant improvement in terms of the capabilities of 2LS in analysing heap-manipulating programs. This is demonstrated on benchmarks taken from the well-known International Competition on Software Verification (SV-COMP) as well as other benchmarks.
|
|
|
Harnessing Forest Automata for Verification of Heap Manipulating Programs
Šimáček, Jiří ; Abdulla, Parosh (oponent) ; Křetínský, Mojmír (oponent) ; Vojnar, Tomáš (vedoucí práce)
This work addresses verification of infinite-state systems, more specifically, verification of programs manipulating complex dynamic linked data structures. Many different approaches emerged to date, but none of them provides a~sufficiently robust solution which would succeed in all possible scenarios appearing in practice. Therefore, in this work, we propose a new approach which aims at improving the current state of the art in several dimensions. Our approach is based on using tree automata, but it is also partially inspired by some ideas taken from the methods based on separation logic. Apart from that, we also present multiple advancements within the implementation of various tree automata operations, crucial for our verification method to succeed in practice. Namely, we provide an optimised algorithm for computing simulations over labelled transition systems which then translates into more efficient computation of simulations over tree automata. We also give a new algorithm for checking inclusion over tree automata, and we provide experimental evaluation demonstrating
|
|
|
Automatizace exoskopické analýzy pomocí zpracování obrazů sedimentárních zrn pořízených elektronovým mikroskopem
Křupka, Aleš ; Křížek,, Marek (oponent) ; Baroňák, Ivan (oponent) ; Říha, Kamil (vedoucí práce)
Práce se zabývá výzkumem metod analýzy obrazu za účelem využití při exoskopické analýze sedimentárních zrn, konkrétně při rozlišování mezi jednotlivými geomorfologickými genezemi, kterými byla tato zrna formována. Obrazy zrn jsou pořízeny pomocí rastrového elektronového mikroskopu. Hlavním přínosem je návrh metodiky, pomocí které je možné exoskopickou analýzu do značné míry automatizovat. Tato metodika pokrývá automatickou segmentaci zrn v obraze, automatickou analýzu zaoblenosti 2D průmětu zrn a rozlišitelnost geomorfologických genezí podle struktury povrchu zrn. V části zabývající se automatickou segmentací byla navržena metoda, která následně umožňuje snadnou manuální korekci výsledků segmentace. Tato metoda je založena na rozdělení a slučování regionů v obrazu. Jednotlivé kroky této procedury byly navrženy tak, aby bylo co nejvíce využito specifických vlastností snímků zachycujících zrna a následně dosaženo co nejlepších výsledků segmentace. V části automatické analýzy zaoblenosti 2D průmětu sedimentárních zrn byl vyhodnocen vliv obrazového rozlišení na výslednou hodnotu zaoblenosti. Dále zde bylo zkoumáno minimální množství sedimentárních zrn, které je nutné analyzovat pro spolehlivé porovnání dvojice geomorfologických genezí na základě míry zaoblenosti. Pro určení tohoto množství byla navržena metoda, která byla experimentálně ověřena. V části automatické analýzy povrchové struktury sedimentárních zrn byla navržena metoda pro rozlišování geomorfologických genezí. Tato metoda využívá nízkoúrovňové texturní příznaky, pomocí kterých lze popsat jednotlivé obrazy sedimentárních zrn. Modely jednotlivých geomorfologických genezí jsou pak tvořeny souborem histogramů reprezentujících četnosti zastoupení různých konfigurací nízkoúrovňových texturních příznaků. Metody navržené v jednotlivých částech práce byly otestovány a vyhodnoceny na základě databáze, která obsahuje vzorky sedimentárních zrn pocházejících z celkem 4 různých geomorfologických genezí (eolická, glaciální, svahová a vulkanická).
|
|
|
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.
|
|
|
Analýza časového vývoje léčených nádorů páteře v CT datech
Nohel, Michal ; Jan, Jiří (oponent) ; Jakubíček, Roman (vedoucí práce)
Tato diplomová práce se zabývá časovým vývojem léčených nádorů páteře v CT datech. V teoretické části se zabývá anatomií, fyziologií a patofyziologií páteře a těl obratlů. Dále popisuje diagnostické a terapeutické možnosti detekce a léčby nádorů páteře. Její součástí je přehled současného stavu využití časové analýzy v onkologii. Jsou diskutovány problémy dostupných anotací a jsou vytvořeny nové databáze pro následnou analýzu. Dále je navržena metodologie časové analýzy podle tvarové charakterizace a velikosti postižení obratle. Na vytvořené databáze jsou aplikovány navržené metodické přístupy extrakce příznaků. Jejich volba a vhodnost je diskutována, včetně jejich potenciálu pro případné využití pro klinickou praxi sledování vývoje a odvozování charakteristických závislostí příznaků na prognóze pacienta.
|
|
|
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.
|
host ::
RSS.