|
|
Negation in Fuzzy Logic
Dekrét, Lukáš ; Havlena, Vojtěch (referee) ; Křena, Bohuslav (advisor)
This thesis deals with fuzzy logical connections, mainly negations, their properties and constructions.We focused our attention on triangular norms and conorms, which are often used for modeling of fuzzy conjunction and disjunction.We showed the possibilities of constructions of triangular norm and conorm using involutive negations.Futhermore, we dealed with approximation of function, which was created using empirical data to well known fuzzy negator.
|
|
|
Efficient Reduction of Finite Automata
Molnárová, Veronika ; Havlena, Vojtěch (referee) ; Lengál, Ondřej (advisor)
Konečný stavový automat je matematický model popisujúci stroj vykonávajúci výpočet na zadanom vstupe cez postupnosť stavov. Za posledné storočie si tento koncept našiel využitie v rôznych odvetviach informatiky od správania postáv vo videohrách po kompilátory. Pokým automat popisuje jeden jazyk, ten môže byť reprezentovaný nekonečným množstvom rôznych automatov. Keďže veľkosť týchto automatov sa líši, pre zaistenie čo najefektívnejšej práce chceme nájsť ten najmenší z nich. V tejto práci sa pozrieme na päť rôznych typov redukcie automatov. Najskôr sa budeme zaoberať troma známymi redukčnými algoritmami, menovite to bude minimalizácia deterministického automatu, redukcia pomocou relácie simuláciu a redukcia pomocou prevodu na kanonický reziduálny automat. Tieto redukcie boli implementované v jazyku C++ a otestované na skúšobnom vzorku automatov pre porovnanie výsledkov jednotlivých redukcií. Posledne sme sa pozreli na možnosť redukovať konečný stavový automat pomocou SAT a QBF solverov. Vytvorili sme množinu pravidiel pre každý solver pre tvorbu klauzule v konjunktnej normálnej forme, ktorá dokáže jednoznačne reprezentovať automat v Booleovej algebre. S využitím tohto faktu sme vytvorili nový spôsob redukcie nedeterministického automatu.
|
|
|
Plugin for a Code Risk Analysis
Kvasnička, Jaroslav ; Lengál, Ondřej (referee) ; Havlena, Vojtěch (advisor)
Tato práce se zabývá významem analýzy a testování kódu a jeho dopadem na funkčnost a náklady programu. Pojednává o základních principech a typech testování se zaměřením na statickou analýzu. Zkoumá také platformu Eclipse a zásuvné moduly a architekturu cílového kódu. Dále jsme probrali a implementovali rozšíření statického analyzátoru MFB, který byl vyvinut společností BOC-GROUP, spolu s rozšířeními, jako je kontrola Log4j a analyzátor GDPR. Navrhli jsme a implementovali také zásuvný modul pro Eclipse, který dokáže zvýraznit výsledky analyzátoru MFB v prostředí Eclipse IDE. V závěru jsou také diskutována možná budoucí rozšíření, včetně detektorů škodlivých regulárních výrazů a prevence XSS.
|
|
|
Beyond Register Automata: Pushing the Border of Decidability
Gulčíková, Sabína ; Havlena, Vojtěch (referee) ; Lengál, Ondřej (advisor)
Registrový automat (RA) pracujúci nad nekonečnou abecedou je jedným z nástrojov pre pattern matching s backreferenciami, dynamickú verifikáciu, alebo modelovanie paralelných výpočtov. Súčasné riešenia v aplikáciách pattern matchingu používajú backtrackingové algoritmy v prípade nedeterministických regulárnych výrazov. Nemožnosť determinizovať registrový automat spôsobuje, že nie je vhodným formálnym modelom pre riešenie problémov spojených s neefektívnymi aplikáciami backtrackingových algoritmov. Na druhej strane, vybavenosť konečnou pamäťou slúži ako vhodná báza pre ukladanie takzvaných capture groups použitých v takejto aplikácii. Táto práca sa zaoberá predstavením formálneho modelu registrovo množinového automatu. Veľká trieda registrových automatov môže byť transformovaná do tohto deterministického modelu, ktorý okrem iného, dovoľuje vykonávať rýchly pattern matching s backreferenciami. Definované sú vlastnosti zahŕňajúce rozhodnutelnosť testu prázdnosti, determinizovateľnosť, uzavretosť voči Booleovským operáciám. Zároveň tento model porovnávame voči iným registrovým modelom z hľadiska ich vyjadrovacej sily.
|
|
|
Efficient Automata Techniques and Their Applications
Havlena, Vojtěch ; Jančar, Petr (referee) ; Mayr, Richard (referee) ; Esparza, Javier (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zabývá vývojem efektivních technik pro konečné automaty a jejich aplikace. Zejména se věnujeme konečným automatům použitých pří detekci útoků v síťovém provozu a automatům v rozhodovacích procedurách a verifikaci. V první části práce navrhujeme techniky přibližné redukce nedeterministických automatů, které snižují spotřebu zdrojů v hardwarově akcelerovaném zkoumání obsahu paketů. Druhá část práce je je věnována automatům v rozhodovacích procedurách, zejména slabé monadické logice druhého řádů k následníků (WSkS) a teorie nad řetězci. Navrhujeme novou rozhodovací proceduru pro WS2S založenou na automatových termech, umožňující efektivně prořezávat stavový prostor. Dále studujeme techniky předzpracování WSkS formulí za účelem snížení velikosti konstruovaných automatů. Automaty jsme také aplikovali v rozhodovací proceduře teorie nad řetězci pro efektivní reprezentaci důkazového stromu. V poslední části práce potom navrhujeme optimalizace rank-based komplementace Buchiho automatů, které snižuje počet generovaných stavů během konstrukce komplementu.
|
|
|
Just-in-Time Compilation of Dependently-Typed Lambda Calculus
Zárybnický, Jakub ; Havlena, Vojtěch (referee) ; Lengál, Ondřej (advisor)
Řada programovacích jazyků byla schopna zvýšit svoji rychlost výměnou běhových systémů stavěných na míru za obecné platformy, které pro optimalizaci používají just-in-time překlad, jako jsou GraalVM nebo RPython. V této práci vyhodnocuji, zda je použití takovýchto platforem vhodné i pro jazyky se závislymi typy nebo důkazovými systémy. Tato práce představuje koncepty -kalkulu a teorie typů potřebné pro úvod do závislých typů s relevantními algoritmy, specifikuje malý závisle typovaný jazyk založený na $\lambda\Pi$ kalkulu, a prezentuje dva interpretery tohoto jazyka. Tyto interpretery jsou psané v jazyce Kotlin, první je jednoduchý, psaný ve funkcionálním stylu a druhý používá platformu GraalVM a Truffle. GraalVM je platforma založená na virtuálním stroji Javy (JVM), která přidává just-in-time překladač založený na částečném vyhodnocení (partial evaluation) a Truffle je knihovna pro tvorbu programovacích jazyků využívající tento překladač. Závěr práce vyhodnocuje běhové charakteristiky těchto interpreterů na různých zátěžových testech.Závěry práce jsou ale silně negativní. Vliv JIT překladu není znatelný ani přes snahu optimalizovat běžné algoritmy z teorie typů, které jsou zjevně nevhodné pro platformu JVM. Práce končí návrhy několika navazujících projektů, které by lépe využily možnosti Truffle a které by byly vhodnější pro implementaci závisle typovaných jazyků.
|
|
|
Reducing Size of Nondeterministic Automata with SAT Solvers
Šedý, Michal ; Havlena, Vojtěch (referee) ; Holík, Lukáš (advisor)
Nedeterministické konečné automaty (NKA) jsou široce využívány v počítačové vědě, například v oblasti formálních jazyků pro reprezentaci regulárních jazyků, k monitorování vysokorychlostních sítí, rozpoznávání obrazu, modelování hardware, nebo dokonce v bioinformatice pro vyhledávání sekvencí nukleotidových kyselin v DNA. NKA jsou také používány v abstraktním regulárním model checkingu, dále ve verifikaci programů manupulujících s řetězci, ve verifikaci programů využívajících ukazatele, pro konstrukci lineárních rovnic a nerovnic, v rozhodovacích procedurách WS1S a WS2S logiky a mnohých dalších. Minimalizace automatů je základní technikou, která pomáhá snižovat nároky na zdroje (paměť, čas nebo množství hardwarových komponentů) a urychlovat operace prováděné na automatech. Běžně používané minimalizační techniky, jakými jsou slučování stavů, odstraňování hran přechodů nebo saturace, mohou v automatech zanechat potenciální minimalizovatelné podgrafy obsahující duplicitní jazykovou informaci. Tyto fragmenty sestávají ze skupiny stavů, kde je již část jazyka jednoho stavu pokryta jazyky ostatních stavů z této skupiny. Tato práce popisuje novou techniku využívající SAT solver, který poskytuje informaci umožňující minimalizovat tyto doposud neminimalizovatelné části automatů. Nově vyvíjená metoda, která využívá pouze informaci od SAT solveru a slučování stavů minimalizuje automaty podobně efektivně, a v případě automatů s nízkým počtem přechodů dokonce rychleji než nástroj RABIT/Reduce, který využívá slučování stavů a odstraňování hran.
|
|
|
Construction of Effective Automata for Regex Matching in HW
Frejlach, Jakub ; Havlena, Vojtěch (referee) ; Češka, Milan (advisor)
This thesis is motivated by the application of REs in domains requiring fast matching such has deep packet inspections. To ensure sufficient speed a HW acceleration is typically employed. During the acceleration, REs are in the form of NFA synthesized on FPGA. Although HW acceleration solves the speed problems, it suffers from increased consumption of the FPGA components, specifically LUT. The goal of this thesis is to design, implement and experimentally evaluate heuristic method for approximation of FA in context of HW accelerated RE matching. The purpose of this approximation is to lower consumption of LUT components during FPGA synthesis. The key idea of the method is to add some transitions allowing to construct a smaller number of character classes and thus to reduce the number of LUT implementing the transition relation while reducing the error by modifying only less significant parts of FA. Proposed method together with evaluation pipeline is implemented in TOFA tool. Technique was evaluated on both synthetic and real data. Results of experiments shows, that transitional approximation works especially well on automatas with large number of equivalence character classes.
|
|
|
An Automatic Theorem Prover
Mazánek, Martin ; Havlena, Vojtěch (referee) ; Lengál, Ondřej (advisor)
This thesis focuses on implementation of resolution-based automatic theorem prover for propositional and first-order logic. The goal of this thesis is to create simple prover and document the development. Making state-of-the-art prover is not the goal of this thesis. We also present some popular automated theorem provers.
|
|
|
A Haskell Platform for Creating Progressive Web Applications
Zárybnický, Jakub ; Havlena, Vojtěch (referee) ; Lengál, Ondřej (advisor)
Tato práce se snaží usnadnit vývoj webových aplikací psaných v programovacím jazyce Haskell vytvořením sady komponent, které zatím chybí v jeho ekosystému knihoven, se zaměřením na komponenty nutné pro tvorbu Progressive Web Applications, aplikace, které používají nové technologie jako např. Service Workers. Tato práce porovnává, které komponenty se očekávají od webových platforem a které jsou dostupné pro Haskell; popisuje implementaci tří komponent (knihovny pro routování, úložiště a Service Workery); a implementuje tři aplikace, které demonstrují použití těchto komponent.
|
guest ::
