|
|
String Constraint Solving Through Parikh Images
Bartoš, Petr ; Havlena, Vojtěch (oponent) ; Holík, Lukáš (vedoucí práce)
This bachelor thesis aims to implement an alternative way of solving string constraints using the so-called flattening algorithm. The algorithm makes use of Parikh images and parametric flat automata to effectively convert string constraints to linear arithmetic, which allows for leveraging powerful SMT solvers. Solving constraints as an algebraic problem is supposed to be more efficient than standardly used automata-based techniques, as it avoids common pitfalls, such as state-space exposion. The thesis covers the theoretical knowledge required to understand the flattening algorithm and introduces alternative modern solution strategies. The implementation results are then compared to other solvers using conventional competition benchmarks. The conducted experiments show that while the speed of the implementation compared to other state-of-the-art solvers is worse, the effectiveness of the underapproximation itself is fairly promising, thus yielding mixed results.
|
|
|
Spojování záznamů v genealogických datech
Šorm, Jan ; Rozman, Jaroslav (oponent) ; Zbořil, František (vedoucí práce)
Hlavním cílem této bakalářské práce je studium genealogických dat, zjištění možných problému při jejich slučování a implementace metod pro toto slučování dat. V této práci se bude především studovat problematika třídění podobných tvarů jmen do společných tříd. Tento problém se bude studovat zejména proto, že v každém matričním záznamu hrají nejdůležitější roli jména a příjmení dotčených osob a jejich příbuzných. V práci tedy bude rozebráno několik metrik pro výpočet vzdálenosti mezi dvěma řetězci. Dále pak pro tyto metriky bude provedeno několik experimentů, které budou mít za cíl roztřídit jména do tříd s co nejmenším počtem chyb. Na základě těchto výsledků pak budou provedeny i experimenty pro samotné slučování jednotlivých genealogických záznamů.
|
|
|
Spojování záznamů v genealogických datech
Šorm, Jan ; Rozman, Jaroslav (oponent) ; Zbořil, František (vedoucí práce)
Hlavním cílem této bakalářské práce je studium genealogických dat, zjištění možných problému při jejich slučování a implementace metod pro toto slučování dat. V této práci se bude především studovat problematika třídění podobných tvarů jmen do společných tříd. Tento problém se bude studovat zejména proto, že v každém matričním záznamu hrají nejdůležitější roli jména a příjmení dotčených osob a jejich příbuzných. V práci tedy bude rozebráno několik metrik pro výpočet vzdálenosti mezi dvěma řetězci. Dále pak pro tyto metriky bude provedeno několik experimentů, které budou mít za cíl roztřídit jména do tříd s co nejmenším počtem chyb. Na základě těchto výsledků pak budou provedeny i experimenty pro samotné slučování jednotlivých genealogických záznamů.
|
|
|
String Analysis for Code Contracts
Dort, Vlastimil ; Parízek, Pavel (vedoucí práce) ; Kofroň, Jan (oponent)
Jedním ze způsobů prevence chyb v objektově orientovaných programech je používání kontraktů, kterými jsou například vstupní a výstupní podmínky metod nebo invarianty tříd. Ve frameworku .NET je používání kontraktů umožněno díky frameworku Code Contracts, který mimo jiné obsahuje nástroj Clousot na statickou analýzu programů, založený na abstraktní interpretaci. Ačkoli řetězce jsou jedním ze základních typů v programech pro .NET, Clousot neobsahuje použitelnou podporu pro analýzu řetězcových hodnot. V této práci probereme specifika práce s řetězci v jazyce C# a frameworku .NET a ukážeme, jak je možné ji pokrýt statickou analýzou. Zvolený přístup využívá metody třídy String a omezenou podmnožinu regulárních výrazů ke specifikaci vlastností řetězců v kódu, a abstraktní interpretaci s nerelačními abstraktními doménami k důkazům těchto vlastností. Zvolili jsme několik již publikovaných abstraktních domén pro řetězce, které se mezi sebou liší složitostí a schopností reprezentovat různé vlastnosti řetězců. Tyto domény jsme adaptovali pro zvolené prostředí, což zahrnovalo definici abstraktní sémantiky pro podporované řetězcové operace. Abstraktní domény jsme implementovali v nástroji Clousot, a to tak, aby bylo v budoucnu možné rozšíření o další domény. Powered by TCPDF (www.tcpdf.org)
|
|
|
Maloobchod v Kazachstánu
Shaibakov, Timur ; Filipová, Alena (vedoucí práce) ; Zeman, Jiří (oponent)
Táto práce je věnovana popisu maloobchodu Kazachstánu včetně analyzy jeho specifik, historii a dnešního stavu. Důraz v prácí je takě kláden na analyzu trhu nákupních center a budoucím trendům v kazašském maloobchodu v kontextu vstupu Kazachstánu do celní unie s Ruskem a Běloruskem.
|
|
| |
|
|
Markovské procesy a jejich řešení v MS Excel
Löw, Alexandr ; Kořenář, Václav (vedoucí práce) ; Šindelářová, Irena (oponent)
Markovské procesy jsou stochastické procesy modelující chování jednotek, které není pevně dané. Známe pouze pravděpodobnosti s jakými tyto jednotka přecházejí mezi jednotlivými stavy. Analýza těchto procesů je z velké části založena na násobení matic, což může být, zvláště u většího počtu stavů, při ručním výpočtu složité a časově náročné. Proto jsou tyto výpočty prováděny za pomocí počítačů. Cílem této práce je zpracování aplikace, která by v prostředí MS Excel tyto výpočty realizovala a uživateli pak v přehledné formě prezentovala výsledky. Tato aplikace analyzuje jak absorpční, tak i regulární markovské řetězce. Aplikace je primárně určena pro použití při výuce stochastických modelů.
|
|
|
Aplikace internetu v cestovním ruchu
Daniš, Michal ; Jakubíková, Dagmar (vedoucí práce) ; Blinka, Roman (oponent)
Bakalářská práce se věnuje cestovnímu ruchu a internetu jako jednomu z nástrojů, který je aplikován v marketingu cestovního ruchu. Teoretická část obsahuje definice cestovního ruchu, příčiny jeho vzniku a postavení v národním hospodářství, historii a vývoj internetu. Praktická část mapuje aplikaci internetu při prodeji služeb hotelových řetězců, leteckých společností, autobusové a vlakové dopravy, při prodeji služeb cestovních kanceláří a agentur, ale i v individuální dopravě a turistice.
|
host ::
RSS.