|
|
Automata in Infinite-state Formal Verification
Lengál, Ondřej ; Jančar, Petr (referee) ; Veith, Helmut (referee) ; Esparza, Javier (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zaměřuje na konečné automaty nad konečnými slovy a konečnými stromy, a použití těchto automatů při formální verifikaci nekonečně stavových systémů. Práce se nejdříve věnuje rozšíření existujícího přístupu pro verifikaci programů které manipulují s haldou (konkrétně programů s dynamickými datovými strukturami), jenž je založen na stromových automatech. V práci je navrženo několik rozšíření tohoto přístupu, jako například jeho plná automatizace či jeho rozšíření o podporu uspořádaných dat. V práci jsou popsány nové rozhodovací procedury pro dvě logiky, které jsou často používány ve formální verifikaci: pro separační logiku a pro slabou monadickou druhořádovou logiku s následníkem. Obě tyto rozhodovací procedury jsou založeny na převodu jejich problému do automatové domény a následné manipulaci v této cílové doméně. Posledním přínosem této práce je vývoj nových algoritmů k efektivní manipulaci se stromovými automaty, s důrazem na testování inkluze jazyků těchto automatů a manipulaci s automaty s velkými abecedami, a implementace těchto algoritmů v knihovně pro obecné použití. Tyto vyvinuté algoritmy jsou použity jako klíčová technologie, která umožňuje použití výše uvedených technik v praxi.
|
|
|
Automation of Exoscopic Analysis Using Image Processing of Sedimentary Grains Acquired by Electron Microscope
Křupka, Aleš ; Křížek,, Marek (referee) ; Baroňák, Ivan (referee) ; Říha, Kamil (advisor)
This thesis deals with image analysis methods which can be exploited in exoscopic analysis of sedimentary grains, specifically for the purpose of distinguishing between geomorphologic geneses which influenced a form of sedimentary grains. The images of sedimentary grains were acquired by a scanning electron microscope. The main contribution is the proposal of multiple methods that can significantly automate the exoscopic analysis. These methods cover the automatic segmentation of grains in image, the automatic analysis of roundness of 2D grain projection and the classification of geomorphologic geneses according to the grain surface structure. In the section concerning the automatic segmentation, a segmentation method enabling an easy subsequent manual result correction was proposed. This method is based on the split-and-merge approach. The individual steps the procedure were designed to exploit specific properties of sedimentary grain images in order to obtain the best segmentation results. In the section concerning the automatic roundness analysis of 2D projection of sedimentary grains, an influence of pixel resolution on a result roundness value was evaluated. Further, a minimal number of grains, which is necessary to analyze in order to reliably compare a pair of geomorphological geneses, was investigated. For the determination of this number, a method was proposed and experimentally verified. In the section of automatic analysis of sedimentary grain surface structure, a method for classification of geomorphologic geneses was proposed. The method utilizes low-level texture features which describes individual images of sedimentary grains. A model of geomorphological genesis is constituted of a set of histograms representing occurrences of different configurations of low-level texture features. The methods proposed in the thesis were tested and evaluated based on a database, which consists of sedimentary grain samples from 4 different geomorphological geneses (eolic, glacial, slope and volcanic).
|
|
|
Analysis of C Programs with Dynamic Linked Data Structures
Šoková, Veronika ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
This master's thesis deals with the analysis of dynamic linked data structures using shape analysis used in the Predator tool. It describes the chosen abstract domain for heap representation - symbolic memory graphs. It deals with the design of framework for the development of static analyzers based on Clang/LLVM. The main contribution is implementing and testing LLVM's transformation passes that simplify the LLVM IR. Second contribution is the optimization of parameters for parallel run of several variants of the Predator tool. Parameters are tuned for benchmark from SV-COMP'16, where our tool won gold medal in Heap Data Structures category. Last contribution is the design of verification core with the focus on the SMG domain.
|
|
|
Creation of Database and Classification of Diatoms
Svoboda, Jan ; Nötzel, Ralf (referee) ; Drahanský, Martin (advisor)
Výsledná aplikace pracuje s vytvořenou databází, obsahující obrázky jednotlivých rozsivek a informace o nich uložené v XML dokumentu. Nad touto databází jsou zajištěny základní operace přidávání, úpravy, mazání a vyhledávání. Vyhledávání může probíhat třemi způsoby, a to pomocí textových vstupů, obrázkových vstupů nebo jejich kombinací. Algoritmus vyhledávání pomocí obrázkových vstupů se snaží najít v databázi co nejpodobnější kandidáty s ohledem na tvar a tloušťku schránky rozsivky a na vnitřní strukturu rozsivky jako takové. Toto vyhledávání je nejčastěji znepřesněno kvalitou pořízených snímků, či obrázků porovnávaných rozsivek. Program obsahuje přehledné a intuitivní grafické rozhraní, jež nám pohodlně umožňuje prohlížet stávající databázi a provádět operace nad ní s možností nastavení filtrovacích hodnot při vyhledávání.
|
guest ::
