|
|
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.
|
|
|
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.
|
|
|
Time development analysis of treated lesion in spinal CT data
Nohel, Michal ; Jan, Jiří (referee) ; Jakubíček, Roman (advisor)
This diploma thesis is focused on time-development analysis of treated lesion in CT data. The theoretical part of the thesis deals with the anatomy, physiology, and pathophysiology of the spine and vertebral bodies. It further describes diagnostic and therapeutic options for the detection and treatment of spinal lesions. It contains an overview of the current state of usage of time-development analysis in oncology. The problems of the available databases are discussed and new databases are created for subsequent analysis. Futhermore, the methodology of time-development analysis according to the shape characterization and the size of the vertebral involvement is proposed. The proposed methodological approaches to feature extraction are applied to the created databases. Their choice and suitability is discussed, including their potential for possible usege in clinical practice of monitoring the development and derivation of characteristic dependences of features on the patient's prognosis.
|
|
|
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í.
|
|
|
Template-Based Synthesis of Heap Abstractions
Malík, Viktor ; Hruška, Martin (referee) ; Vojnar, Tomáš (advisor)
Cieľom tejto práce je návrh analýzy tvaru haldy vhodnej pre potreby analyzátora 2LS. 2LS je nástroj pre analýzu C programov založený na automatickom odvodzovaní invariantov s použitím SMT solvera. Navrhované riešenie obsahuje spôsob reprezentácie tvaru programovej haldy pomocou logických formulí nad teóriou bitových vektorov. Tie sú následne využité v SMT solveri pre predikátovú logiku prvého rádu na odvodenie invariantov cyklov a súhrnov jednotlivých funkcií analyzovaného programu. Náš prístup je založený na ukazateľových prístupových cestách, ktoré vyjadrujú dosiahnuteľnosť objektov na halde z ukazateľových premenných. Informácie získané z analýzy môžu byť využité na dokázanie rôznych vlastností programu súvisiacich s prácou s dynamickýcmi dátovými štruktúrami. Riešenie bolo implementované v rámci nástroja 2LS. S jeho použitím došlo k výraznému zlepšeniu schopnosti 2LS analyzovať programy pracujúce s ukazateľmi a dynamickými dátovými štruktúrami. Toto je demonštrované na sade experimentov prevzatých zo známej medzinárodnej súťaže vo verifikácii programov SV-COMP a iných experimentoch.
|
|
|
Harnessing Forest Automata for Verification of Heap Manipulating Programs
Šimáček, Jiří ; Abdulla, Parosh (referee) ; Křetínský, Mojmír (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zabývá verifikací nekonečně stavových systémů, konkrétně, verifikací programů využívajích složité dynamicky propojované datové struktury. V minulosti se k řešení tohoto problému objevilo mnoho různých přístupů, avšak žádný z nich doposud nebyl natolik robustní, aby fungoval ve všech případech, se kterými se lze v praxi setkat. Ve snaze poskytnout vyšší úroveň automatizace a současně umožnit verifikaci programů se složitějšími datovými strukturami v této práci navrhujeme nový přístup, který je založen zejména na použití stromových automatů, ale je také částečně inspirován některými myšlenkami, které jsou převzaty z metod založených na separační logice. Mimo to také představujeme několik vylepšení v oblasti implementace operací nad stromovými automaty, které jsou klíčové pro praktickou využitelnost navrhované verifikační metody. Konkrétně uvádíme optimalizovaný algoritmus pro výpočet simulací pro přechodový systém s návěštími, pomocí kterého lze efektivněji počítat simulace pro stromové automaty. Dále uvádíme nový algoritmus pro testování inkluze stromových automatů společně s experimenty, které ukazují, že tento algoritmus překonává jiné existující přístupy.
|
|
|
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).
|
|
|
Automata in Decision Procedures and Performance Analysis
Fiedor, Tomáš ; Barnat, Jiří (referee) ; Radu, Iosif (referee) ; Vojnar, Tomáš (advisor)
Tato práce se věnuje vylepšení současného stavu formalní analýzy a verifikace založené na automatech a zaměřené na systémy s nekonečnými stavovými prostory. V první části se práce zabývá dvěma rozhodovacími procedurami pro logiku WS1S, které jsou založené na korespondenci mezi formulemi logiky WS1S a konečnými automaty. První metoda je založena na tzv. antiřetězcích, ale, je limitována pouze na formule v prenexním normálním tvaru. Následně je tento přístup zobecněn na libovolné formule, jsou zavedeny tzv. jazykové termy a na jejich základě je navržena nová procedura, která pracuje za běhu a zpracovává tyto termy "líným" způsobem. Abychom získali efektivní rozhodovací proceduru, je dále navržena sada optimalizací (přičemž některé nejsou limitovány pouze pro naše přístupy). Obě metody jsou srovnány s ostatními nástroji implementujícími různé známé rozhodovací procedury. Získané výsledky jsou povzbuzující a ukazují, že použitelnost logiky WS1S je možno rozšířit na širší třídu formulí. V druhé části se práce zabývá analýzou mezí zdrojů programů manipulujících s haldou. Je zde navržena nová třída tzv. tvarových norem založených na délkách cest mezi význačnými místy na haldě, které jsou automaticky odvozovány z analyzovaného programu. Na základě této třídy norem je dále navržen kalkul, který je schopen přesně odvodit změny odvozených normů a použít je k vygenerování odpovídající celočíselné reprezentace vstupního programu, která je následně využita pro následovanou dedikovanou analýzou mezí zdrojů. Tato metoda byla implementována nad analýzou tvaru založenou na tzv. lesních automatech, implementovanou v nástroji Forester, a dále byl použit dobře zavedený analyzátor mezí zdrojů, implementovaný v nástroji Loopus. V experimentální evaluaci bylo ukázáno, že je opravdu takto získán silný analyzátor, který je schopen odvodit meze programů, které ještě nikdy plně automatizovaně odvozené nebyly.
|
|
|
Time development analysis of treated lesion in spinal CT data
Nohel, Michal ; Jan, Jiří (referee) ; Jakubíček, Roman (advisor)
This diploma thesis is focused on time-development analysis of treated lesion in CT data. The theoretical part of the thesis deals with the anatomy, physiology, and pathophysiology of the spine and vertebral bodies. It further describes diagnostic and therapeutic options for the detection and treatment of spinal lesions. It contains an overview of the current state of usage of time-development analysis in oncology. The problems of the available databases are discussed and new databases are created for subsequent analysis. Futhermore, the methodology of time-development analysis according to the shape characterization and the size of the vertebral involvement is proposed. The proposed methodological approaches to feature extraction are applied to the created databases. Their choice and suitability is discussed, including their potential for possible usege in clinical practice of monitoring the development and derivation of characteristic dependences of features on the patient's prognosis.
|
|
|
Automata in Decision Procedures and Performance Analysis
Fiedor, Tomáš ; Barnat, Jiří (referee) ; Radu, Iosif (referee) ; Vojnar, Tomáš (advisor)
Tato práce se věnuje vylepšení současného stavu formalní analýzy a verifikace založené na automatech a zaměřené na systémy s nekonečnými stavovými prostory. V první části se práce zabývá dvěma rozhodovacími procedurami pro logiku WS1S, které jsou založené na korespondenci mezi formulemi logiky WS1S a konečnými automaty. První metoda je založena na tzv. antiřetězcích, ale, je limitována pouze na formule v prenexním normálním tvaru. Následně je tento přístup zobecněn na libovolné formule, jsou zavedeny tzv. jazykové termy a na jejich základě je navržena nová procedura, která pracuje za běhu a zpracovává tyto termy "líným" způsobem. Abychom získali efektivní rozhodovací proceduru, je dále navržena sada optimalizací (přičemž některé nejsou limitovány pouze pro naše přístupy). Obě metody jsou srovnány s ostatními nástroji implementujícími různé známé rozhodovací procedury. Získané výsledky jsou povzbuzující a ukazují, že použitelnost logiky WS1S je možno rozšířit na širší třídu formulí. V druhé části se práce zabývá analýzou mezí zdrojů programů manipulujících s haldou. Je zde navržena nová třída tzv. tvarových norem založených na délkách cest mezi význačnými místy na haldě, které jsou automaticky odvozovány z analyzovaného programu. Na základě této třídy norem je dále navržen kalkul, který je schopen přesně odvodit změny odvozených normů a použít je k vygenerování odpovídající celočíselné reprezentace vstupního programu, která je následně využita pro následovanou dedikovanou analýzou mezí zdrojů. Tato metoda byla implementována nad analýzou tvaru založenou na tzv. lesních automatech, implementovanou v nástroji Forester, a dále byl použit dobře zavedený analyzátor mezí zdrojů, implementovaný v nástroji Loopus. V experimentální evaluaci bylo ukázáno, že je opravdu takto získán silný analyzátor, který je schopen odvodit meze programů, které ještě nikdy plně automatizovaně odvozené nebyly.
|
guest ::
