|
|
Heuristics in String Solving
Řezáč, Michal ; Havlena, Vojtěch (oponent) ; Síč, Juraj (vedoucí práce)
This work aims on identifying heuristics and strategies used in modern string solvers and evaluating their impact on the effectiveness of the solving. In particular, two solvers -- cvc5 and Z3 -- are examined. The thesis describes the techniques used by SMT solvers and the strategies implemented by string solvers. The evaluation of the effectiveness of the heuristics was performed by disabling them directly in the code of the tools mentioned and then evaluating the impact on solving the sets of standard benchmarks. The result of this work is summary of a set of specific heuristics and a description of the structure of the tools cvc5 and Z3. The measurements failed to demonstrate the actual impact of the heuristics identified and described.
|
|
|
Formal Models for Data Languages
Vašák, Jan ; Havlena, Vojtěch (oponent) ; Lengál, Ondřej (vedoucí práce)
Data words are a common way to formally work with words over infinite alphabets. In practice, an infinite alphabet can represent an actually infinite set, such as the integers or a set of strings, or a large finite set, such as the Unicode symbols. We explore some theoretical properties of register set automata, a data word model that, crucially, can be used as a means to determinise a large class of register automata (this allows, e.g., for a deterministic automata representation of a class of regexes with back-references). We also extend streaming data string transducers, a model designed to represent a class of list-processing programs, with set-registers. This extension can, for example, represent a program that removes duplicates from a list, which is not representable using the base model. We then show that this extension’s functional equivalence problem is decidable. Lastly, a prototype regex matcher based on register set automata was implemented, and we experimentally show that it performs well under regular expression denial of service attacks that can cripple other matchers used in practice.
|
|
|
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.
|
|
|
Length Constraints in String Solving
Hranička, Jan ; Lengál, Ondřej (oponent) ; Havlena, Vojtěch (vedoucí práce)
String solving is currently a fundamental part of formal verification with numerous scientific and business applications. In this thesis, a new decision procedure is proposed with the intend to extend a state-of-the-art string solver Z3-Noodler. This decision procedure is based on symbolically aligning string variables in word equations by generating constraints on their lengths. When experimenting with this procedure on standardized benchmarks, its integration with Z3-Noodler resulted in the reduction of 32 timeouts and in some instances more than 50x time improvement. These benefits make it possible for this decision procedure to be included in a future release of the mentioned solver.
|
|
|
Simulation and Analysis of Quantum Circuits
Jobranová, Sára ; Havlena, Vojtěch (oponent) ; Lengál, Ondřej (vedoucí práce)
Simulation of quantum circuits is a key tool for future advancements in the promising field of quantum computing. Due to the fact that this task is very computationally demanding, the performance of state-of-the-art simulators on more complex circuits is still far from satisfactory. In this thesis, we propose a new approach to simulate quantum circuits and present an implementation based on this approach. Our simulation technique allows for accurate simulation and is based on multi-terminal binary decision diagrams. We extended the usual process of a decision diagram-based simulation by symbolic execution of repeating structures in a quantum circuit (such as loops), where we compute the big-step semantics of this structure and do not re-evaluate the gates. We show that symbolic loop execution significantly accelerates the simulation and that the implemented tool is not only competitive with other state-of-the-art simulators, but also greatly outperforms the state of the art for many quantum circuits.
|
|
|
Aproximativní techniky pro Markovovy modely
Andriushchenko, Roman ; Havlena, Vojtěch (oponent) ; Češka, Milan (vedoucí práce)
Předkládaná práce je zaměřena na popis aproximativních technik pro analýzu Markovských řetězců, konkrétně na metody založené na agregaci nebo ořezávání stavového prostoru. Na začátku je představen postup umožňující aplikaci agregace pro modely diskrétního času s libovolnou strukturou stavového prostoru a je odvozen lepší odhad aproximační chyby. Daný postup je pak propojen s uniformizačními technikami, jak se standardní tak s adaptivní, což umožňuje provádět analýzu řetězců spojitého času spolu s odhadem aproximační chyby. Navržená technika spolu s existujícími metodami založenými na ořezávání byly implementovány v rámci nástroje PRISM. Provedené experimenty potvrzuji, že nově odvozený odhad aproximační chyby vylepšuje přesnost o několik řádů bez zhoršení celkové výkonnosti. Je ukázano, že výsledná agregační metoda je schopna poskytnout validní aproximaci modelu spolu s adekvátními odhady aproximační chyby, a to jak v diskrétním tak i ve spojitém čase. Následně je provedeno porovnání s technikami založenými na ořezávání stavového prostoru a je diskutováno pro které třídy Markovských řetězců je ta či ona metoda použitelnější. Nakonec je demonstrováno úspěšne použití aproximativních technik pro model checking Markovových modelů.
|
|
|
Porovnávání jazyků a redukce automatů používaných při filtraci síťového provozu
Havlena, Vojtěch ; Rogalewicz, Adam (oponent) ; Vojnar, Tomáš (vedoucí práce)
Tato práce se zabývá porovnáváním jazyků automatů a redukcí automatů používaných při monitorování síťového provozu. Je navrženo několik přístupů pro přibližnou redukci automatů (nezachovávající jazyk) a přístup pro porovnávání jejich jazyků. Redukce jsou založeny na podaproximaci jazyka automatu, kdy dochází k odstraňování stavů nebo na nadaproximaci jazyka, kdy dochází k přidávání nových smyček (a odstranění zbytečných stavů později). Navržené metody pro přibližnou redukci a navržená pravděpodobnostní vzdálenost využívají informaci ze síťového provozu. Jsou poskytnuty formální záruky vzhledem k modelu síťového provozu, který je reprezentován pravděpodobnostním automatem. Metody byly implementovány a jejich vlastnosti byly ověřeny na automatech používaných pro filtrování síťového provozu.
|
|
|
Reducing Size of Nondeterministic Automata with SAT Solvers
Šedý, Michal ; Havlena, Vojtěch (oponent) ; Holík, Lukáš (vedoucí práce)
Nondeterministic finite automata (NFA) are widely used in computer science fields, such as regular languages in formal language theory, high-speed network monitoring, image recognition, hardware modeling, or even in bioinformatic for the detection of the sequence of nucleotide acids in DNA. They are also used in regular mode checking, in string solving, in verification of pointer manipulating programs, for construction of linear arithmetic equations and inequalities, for decision in WS1S and WS2S logic, and many others. Automata minimization is a fundamental technique that helps to decrease resource claims (memory, time, or a number of hardware components) of implemented automata and speed up automata operations. Commonly used minimization techniques, such as state merging, transition pruning, and saturation, can leave potentially minimizable automaton subgraphs with duplicit language information. These fragments consist of a group of states, where the part of language of one state is piecewise covered by the other states in this group. The thesis describes a new minimization approach, which uses SAT solver, which provides information for efficient minimization of these so far nonminimizable automaton parts. Moreover, the newly investigated method, which only uses solver information and state merging, can minimize the automaton similarly and on automata with low transition count faster than a tool RABIT/Reduce, which uses state merging and transition pruning.
|
|
|
A Haskell Platform for Creating Progressive Web Applications
Zárybnický, Jakub ; Havlena, Vojtěch (oponent) ; Lengál, Ondřej (vedoucí práce)
This work attempts to ease developing browser applications in the Haskell programming language by creating a set of components that its library ecosystem so far lacks, especially focusing on the components required for development of Progressive Web Applications, applications that use new technologies like Service Workers. The thesis compares which components are commonly expected from a web framework and which are available in Haskell; describes the implementation of three such components (router, storage, and Service Worker libraries); and implements three applications that demonstrate use of these components.
|
|
|
Konjunkce a disjunkce ve fuzzy logice
Havlena, Vojtěch ; Kunovský, Jiří (oponent) ; Křena, Bohuslav (vedoucí práce)
Tato práce se věnuje triangulárním normám a jejich zobecněním - uninormám, zejména jejich transformacím pomocí jednotkové funkce, a také modelování fuzzy logické konjunkce a disjunkce na základě empirických dat. Byly stanoveny podmínky, při nichž transformací určitých uninorem vznikne opět uninorma. Taktéž byly určeny podmínky invariantnosti transformace pro třídu určitých uninorem. Transformace uninorem rozšiřuje třídu možných spojek a jejich studium nám ulehčilo hledání podmínek při modelování. Byl také nalezen a analyzován algoritmus pro modelování fuzzy logických spojek. Na základě programu implementujícího tento algoritmus byl vyhodnocen experiment, který měl za cíl modelovat fuzzy konjunkci užívanou lidmi.
|
host ::
RSS.