|
|
Heuristics in String Solving
Řezáč, Michal ; Havlena, Vojtěch (referee) ; Síč, Juraj (advisor)
Tato práce se zaměřuje na identifikaci heuristik a strategií použitých v moderních string solverech a na vyhodnocení jejich dopadu na efektivitu řešení. Zkoumány jsou především dva solvery – cvc5 a Z3. Práce popisuje techniky používané SMT solverech a strategie, které implementují string solvery. Vyhodnocení efektivity heuristik bylo prováděno jejich vypínáním přímo v kódu uvedených nástrojů a následným vyhodnocením dopadu na řešení standardních sad benchmarků. Výsledkem této práce je soupis sady konkrétních heuristik a popis struktury nástrojů cvc5 a Z3. Měřením se nepodařilo prokázat, jak velký skutečný dopad identifikované a popsané heuristiky mají.
|
|
|
Formal Models for Data Languages
Vašák, Jan ; Havlena, Vojtěch (referee) ; Lengál, Ondřej (advisor)
Datová slova jsou běžně používaná pro formální práci se slovy nad nekonečnými abecedami. V praxi může nekonečná abeceda modelovat skutečně nekonečnou množinu, např. celá čísla nebo množinu řeťezců, nebo velkou konečnou množinu, jako např. znaky sady Unicode. Tato práce se nejprve věnuje teoretickým vlastnostem registrově množinových automatů. Registrově množinové automaty jsou modelem nad datovými slovy, který lze použít pro determinizaci velké třídy registrových automatů (toto např. umožňuje deterministickou automatovou reprezentaci třídy regulárních výrazů se zpětnými odkazy). Dále jsme rozšířili streaming data string převaděče, model určený pro modelování třídy programů pro zpracování lineárních seznamů, o množinové registry. Toto rozšíření umožňuje např. modelovat program, který odstraní duplicitní hodnoty z lineárního seznamu, což není možné modelovat základními streaming data string převaděči. Ukážeme, že problém funkční ekvivalence je pro toto rozšíření rozhodnutelný. Také byl naimplementován prototyp regex matcheru založený na registrově množinových automatech. Ukážeme, že prototyp si vede dobře pod ReDoS (regular expression denial of service) útoky, které jsou efektivní vůči regex matcherům používaným v praxi.
|
|
|
String Constraint Solving Through Parikh Images
Bartoš, Petr ; Havlena, Vojtěch (referee) ; Holík, Lukáš (advisor)
Tato bakalářská práce si klade za cíl implementovat alternativní způsob řešení řetězcových omezení pomocí takzvaného flattening algoritmu, který pomocí Parikhových obrazů a parametrických plochých automatů transformuje řetězcová omezení na lineární vzorce. Takto vyjádřené omezení je možné řešit pomocí výkonných SMT solverů a předchází problémům spjatým s tradičně používanými metodami založených na automatech, jako je například exploze stavového prostoru. Práce popisuje teoretické znalosti potřebné k pochopení algoritmu pro řešení a představuje další state of the art způsoby řešení. Výsledky implementace jsou poté porovnány s ostatnímy solvery na klasických soutěžních benchmarcích. Provedené experimenty ukazují smíšené výsledky – ač navržené řešení nedosahuje podobné rychlosti jako state-of-the-art solvery, přesnost podaproximačního přístupu je relativně příznivá.
|
|
|
Length Constraints in String Solving
Hranička, Jan ; Lengál, Ondřej (referee) ; Havlena, Vojtěch (advisor)
Řešení řetězcových omezení je v dnešní době základním kamenem formální verifikace s širokým vědeckým i obchodním uplatněním. Přínosem této práce je návrh nové rozhodovací procedury s cílem rozšířit jeden z předních string solverů: Z3-Noodler. Tato rozhodovací procedura je založena na symbolickém zarovnání řetězcových proměnných v rovnicích pomocí generování omezení na jejich délky. Experimenty na standartních benchmarcích ukázaly, že integrace této procedury s nástrojem Z3-Noodler vede ke snížení timeoutů o 32 a na určitých testech snižuje celkovou dobu běhu nástroje více než padesátkrát. Díky těmto přínosům je možné očekávat přidání této procedury do zmíněného nástroje.
|
|
|
Simulation and Analysis of Quantum Circuits
Jobranová, Sára ; Havlena, Vojtěch (referee) ; Lengál, Ondřej (advisor)
Simulace kvantových obvodů je klíčovým nástrojem pro další výzkum v oblasti kvantové výpočetní techniky, která je velmi perspektivní. Jedná se však o velmi výpočetně náročný problém, a z tohoto důvodu jsou i u moderních nástrojů při simulaci komplexních obvodů z hlediska výkonu značné rezervy. V této práci představíme nový přístup k simulaci kvantových obvodů a nástroj implementovaný na základě tohoto přístupu. Tato technika umožňuje přesnou simulaci a je založena na multi-terminálních binárních rozhodovacích diagramech. Také rozšiřuje standardní proces simulace založené na rozhodovacích diagramech o symbolickou exekuci opakujících se struktur v kvantovém obvodě (např. smyček), kdy se spočítá sémantika jednoho opakování této struktury a neprovádíme tudíž opětovné vyhodnocování hradel. Ukázali jsme, že symbolické provádění smyček výrazně urychluje simulaci a že implementovaný nástroj je nejen konkurenceschopný s ostatními nejmodernějšími simulátory, ale také tyto simulátory pro mnoho kvantových obvodů značně překonává.
|
|
|
Approximate Techniques for Markov Models
Andriushchenko, Roman ; Havlena, Vojtěch (referee) ; Češka, Milan (advisor)
In this work we discuss approximative techniques for the analysis of Markov chains, namely, state space aggregation and truncation. First, we focus on the application of the former method for the analysis of discrete-time models: we redesign the clustering algorithm to handle chains with an arbitrary structure of the state space and, most importantly, we improve upon existing bounds on the approximation error. The developed approach is then integrated with uniformisation techniques, in both standard and adaptive forms, to approximate continuous-time models as well as provide estimates of the approximation error. This theoretical framework along with existing truncation-based techniques were implemented within PRISM model checker. Experiments confirm that newly derived bounds provide a several orders of magnitude precision improvement without degrading performance. We show that the resulting aggregating approach can provide a valid model approximation supplied by adequate approximation error estimates, in both discrete and continuous time. Then, we perform a comparative analysis of aggregating and truncating techniques, illustrate how different methods handle various types of models, and identify chains for which aggregating, or truncating, analysis is preferred. Finally, we demonstrate a successful usage of approximative techniques for model checking Markov chains.
|
|
|
Comparing Languages and Reducing Automata Used in Network Traffic Filtering
Havlena, Vojtěch ; Rogalewicz, Adam (referee) ; Vojnar, Tomáš (advisor)
The focus of this thesis is the comparison of languages and the reduction of automata used in network traffic monitoring. In this work, several approaches for approximate (language non-preserving) reduction of automata and comparison of their languages are proposed. The reductions are based on either under-approximating the languages of automata by pruning their states, or over-approximating the language by introducing new self-loops (and pruning redundant states later). The proposed approximate reduction methods and the proposed probabilistic distance utilize information from a network traffic. Formal guarantees with respect to a model of network traffic, represented using a probabilistic automaton are provided. The methods were implemented and evaluated on automata used in network traffic filtering.
|
|
|
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.
|
|
|
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.
|
|
|
Conjuction and Disjunction in Fuzzy Logic
Havlena, Vojtěch ; Kunovský, Jiří (referee) ; Křena, Bohuslav (advisor)
This thesis deals with triangular norms and their generalizations - uninorms, in particular with their transformation using a unit function and also with modeling of fuzzy conjunction and disjunction based on empirical data. The conditions under which transformations of certain uninorms give again uninorms are established. Conditions of invariance transformations for certain class of uninorms are found. Transformations of uninorms extend class of connectives. The study of these transformations faciliates the search of modeling conditions. An algorithm for modeling of fuzzy connectors is also proposed and analyzed. An experiment based on implementation of the algorithm is evaluated. This experiment aims at modeling of fuzzy conjunction for human use.
|
guest ::
