|
|
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.
|
|
|
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.
|
|
|
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.
|
|
|
Geometrická morfometrika tvaru a symetrie květních struktur - ekologický a evoluční význam
Rubešová, Veronika ; Neustupa, Jiří (vedoucí práce) ; Woodard, Kateřina (oponent)
V mé bakalářské práci se zabývám literární rešerší na téma geometrické morfometrie, jejího využití pro zkoumání květních symetrií a ekologických i evolučních významů květní symetrie. V první části přináším popis metod a využití geometrické morfometriky. Druhá část se věnuje popisu hlavních typů květní symetrie. Další části zahrnují morfometrické výzkumy určitých linií. Mnoho studií zahrnuje druhy rostlin z čeledi Brassicaceae. Poslední kapitola shrnuje moderní metody morfologického výzkumu a jejich možnosti využití v budoucích výzkumech.
|
|
|
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.
|
|
|
Surface registrations for topology transfer in geometric morphometry
Dupej, Ján ; Pelikán, Josef (vedoucí práce) ; Telea, Alexandru C. (oponent) ; Váša, Libor (oponent)
Geometrická morfometrie slouží biologům a antropologům pro rigorózní a kvantitativní popis tvarů. Tyhle reprezentace tvaru je možno považovat za statistický vzorek, co dovoluje studovat jeho variabilitu v skupinách a srovnávat ho s dalšími proměnnými. Geometrická morfometrie používá landmarky pro popis tvaru, u každého jedince s konzistentní sémantikou. Obecné trojúhelníkové sítě tuhle konzistenci nemají, proto je potřeba je uměle převést na konzistentní reprezentace. Tato dizertace pojednává o návrhu algoritmu pro sémanticky konzistentní převzorkování trojúhelníkových sítí, vhodné pro statistickou analýzu tvarů. Coherent point drift byl použit pro nerigidní registraci, jejíž výsledek tvoří základ pro převzorkované modely. Tento algoritmus byl úspěšně využit u několika studií. CPD je výpočetně náročný algoritmus, proto byly navrženy metody pro zrychlení jeho inicializace a zpracování. Také navrhujeme rozšíření mapující odchylku modelů od dokonalé symetrie. S touhle informací je možno také pracovat jako se statistickým vzorkem, což nachází aplikace mimo jiné u kvantifikaci patologií. Ruční ořezávaní modelů a slučování vzorků vytváří odlehlé oblasti u povrchů a potenciálně velké rozdíly v hustotě pokrytí vrcholy. Navrhujeme nový algoritmus pro nerigidní registraci povrchů s lepší robustností na tyhle jevy a s...
|
|
|
Geometrická morfometrika tvaru a symetrie květních struktur - ekologický a evoluční význam
Rubešová, Veronika ; Neustupa, Jiří (vedoucí práce) ; Woodard, Kateřina (oponent)
V mé bakalářské práci se zabývám literární rešerší na téma geometrické morfometrie, jejího využití pro zkoumání květních symetrií a ekologických i evolučních významů květní symetrie. V první části přináším popis metod a využití geometrické morfometriky. Druhá část se věnuje popisu hlavních typů květní symetrie. Další části zahrnují morfometrické výzkumy určitých linií. Mnoho studií zahrnuje druhy rostlin z čeledi Brassicaceae. Poslední kapitola shrnuje moderní metody morfologického výzkumu a jejich možnosti využití v budoucích výzkumech.
|
|
|
Correspondence Problem in Geometrics Morphometric Tasks
Krajíček, Václav ; Pelikán, Josef (vedoucí práce) ; Kosinka, Jiří (oponent) ; Sochor, Jiří (oponent)
Název práce: Problém korespondence v úlohách geometrické morfometrie Autor: Václav Krajíček Katedra / Ústav: Katedra software a výuky informatiky Vedoucí doktorské práce: RNDr. Josef Pelikán e-mail vedoucího: pepca@cgg.mff.cuni.cz Abstrakt: Analýza tvaru ve fyzické antropologii, biomedicíně a přidružených oborech je často prováděna s použitím landmarků nebo pomocí měření vzdáleností. Nové technické možnosti dovolují digitalizovat věrný vzhled objektu ve formě trojúhelníkových sítí nebo objemových dat. Tyto digitální obrazy jsou obzvláště užitečné v případech, kdy nemohou být vhodným způsobem použity landmarky k popisu tvaru. Aby bylo možné statisticky analyzovat tvar na vzorku pozorování, které jsou reprezentovány zmíněnými zobrazovacími technikami, musí být identifikovány vzájemně si odpovídající body. Registrace je klíčovým nástrojem k mapování reprezentací tvaru do společné souřadné soustavy, kde se hledají vzájemně si odpovídající body, v případě trojúhelníkových sítí na principu nejbližšího souseda a v případě objemových dat podle překrývajících se bodů. Elastická registrace založená na B-spline interpolaci byla vybrána kvůli své mnohostrannosti, relativní rychlosti a schop- nosti...
|
host ::
RSS.