|
|
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.
|
|
|
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á).
|
|
|
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.
|
|
|
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.
|
host ::
RSS.