|
|
Negace ve fuzzy logice
Dekrét, Lukáš ; Havlena, Vojtěch (oponent) ; Křena, Bohuslav (vedoucí práce)
Táto práca sa venuje fuzzy logickým spojkám, najmä negátorom, ich vlastnostiam a konštrukciám. Zamerali sme sa aj na trojuholníkové normy a konormy, teda na funkcie, ktoré sa často používajú na modelovanie fuzzy konjunkcie a disjunkcie. Ukázali sme možnosti konštrukcie trojuholníkových noriem a konoriem pomocou involutívnych negátorov. Ďalej sa v práci venujeme aproximácii funkcie, vytvorenej na základe empirických dát ku známemu fuzzy negátoru.
|
|
|
Efficient Reduction of Finite Automata
Molnárová, Veronika ; Havlena, Vojtěch (oponent) ; Lengál, Ondřej (vedoucí práce)
A finite state automaton is a mathematical model used to describe a machine that performs a computation on the given input over a series of states. In the last century, it has found many uses in different fields of information technology, from video game character behavior to compilers. While each automaton denotes its language, one language can be represented by an infinite number of different automata. As these automata vary in size, to ensure the most efficient work with them, we want to find the smallest one possible. In this thesis, we are going to look at five different types of automata reductions. Firstly, we will talk about three known reduction algorithms, which are the minimization of deterministic automata, the reduction based on a relation of simulation, and the reduction by transformation into a canonical residual automaton. These reductions were implemented in C++ and tested on a sample set of automata to compare their results. Lastly, we looked at the possibility of reducing finite state automata using Boolean satisfiability problem (SAT) and quantified Boolean formula (QBF) solvers. We are presenting a set of rules for each solver for generating a clause in conjunctive normal form (CNF), which can precisely represent the given automaton in Boolean algebra. We used this fact to create a new method of nondeterministic automata reduction.
|
|
|
Plugin for a Code Risk Analysis
Kvasnička, Jaroslav ; Lengál, Ondřej (oponent) ; Havlena, Vojtěch (vedoucí práce)
This thesis explores the importance of code analysis and testing and its impact on program functionality and cost. It discusses the basic principles and types of testing, with a focus on static analysis. The Eclipse platform and plugins are also examined, along with the architecture of the target code. We then discussed and implemented an extension of the static MFB analyzer which the BOC-GROUP company developed along with extensions such as the Log4j checker and GDPR analyzer. We also designed and implemented the Eclipse plugin which can highlight the results of the MFB analyzer in the Eclipse IDE. In conclusion, future possible extensions are also discussed, including harmful regular expression detectors and XSS prevention.
|
|
|
Beyond Register Automata: Pushing the Border of Decidability
Gulčíková, Sabína ; Havlena, Vojtěch (oponent) ; Lengál, Ondřej (vedoucí práce)
Register automaton (RA) operating over infinite alphabet is one of the great tools for pattern matching with backreferences, runtime verification, or modelling of parallel computation. In case of pattern matching with backreferences, the state-of-the-art matchers make use of backtracking algorithms, whose application causes significant slowdown in case of nondeterministic regular expressions. Since RAs cannot always be determinised, it is an unsuitable model for solution to problems related to inefficient usage of backtracking algorithms. On the other hand, the RA's quality of being equipped by a finite memory serves as a good basis for storing the so-called capture groups used in pattern matching with backreferences. In this work, a formal model called register set automaton (RsA) is proposed. A large class of RAs can be transformed into this deterministic model, which, among other things, allows for fast pattern matching with backreferences. We explore RsA's properties including decidability of emptiness testing, determinisability, closure under Boolean operations and we compare it to other register models in context of their expressive power.
|
|
|
Efficient Automata Techniques and Their Applications
Havlena, Vojtěch ; Jančar, Petr (oponent) ; Mayr, Richard (oponent) ; Esparza, Javier (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis develops efficient techniques for finite automata and their applications. In particular, we focus on finite automata in network intrusion detection and automata in decision procedures and verification. In the first part of the thesis, we propose techniques of approximate reduction of nondeterministic automata decreasing consumption of resources of hardware-accelerated deep packet inspection. The second part is devoted to automata in decision procedures, in particular, to weak monadic second-order logic of k successors (WSkS) and the theory of strings. We propose a novel decision procedure for WS2S based on automata terms allowing one to effectively prune the state space. Further, we study techniques of WSkS formulae preprocessing intended to reduce the sizes of constructed intermediate automata. Moreover, we employ automata in a decision procedure of the theory of strings for efficient handling of the proof graph. The last part of the thesis then proposes optimizations in rank-based Buchi automata complementation reducing the number of generated states during the construction.
|
|
|
Just-in-Time Compilation of Dependently-Typed Lambda Calculus
Zárybnický, Jakub ; Havlena, Vojtěch (oponent) ; Lengál, Ondřej (vedoucí práce)
A number of programming languages have managed to greatly improve their performance by replacing their custom runtime system with general platforms that use just-in-time optimizing compilers like GraalVM or RPython. This thesis evaluates whether such a transition would also benefit dependently-typed programming languages or theorem provers. This thesis introduces the type-theoretic notion of dependent types and the algorithms involved in working with them, specifies a minimal dependently-typed language on the -calculus, and presents the implementation two interpreters for this language: a simple interpreter written in Kotlin, and a second interpreter, also written in Kotlin, that uses the Truffle language implementation framework on the GraalVM platform, which is a partial evaluation-based just-in-time compiler based on the Java Virtual Machine. The performance of these two interpreters is then compared on a number of normalization and elaboration tasks.The results are strongly negative, however, the influence of JIT compilation is not noticeable given the large overhead of the JVM platform. This thesis concludes with a number of alternative projects that would use the capabilities of Truffle better.
|
|
|
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.
|
|
|
Konstrukce efektivních automatů pro rozpoznávání regulárních výrazů v HW
Frejlach, Jakub ; Havlena, Vojtěch (oponent) ; Češka, Milan (vedoucí práce)
Motivací této bakalářské práce je užití rozpoznávání regulárních výrazů v aplikačních doménách, kde je vyžadováno rychlé rozpoznávání jako například v hloubkové kontrole paketů. Během akcelerace jsou regulární výrazy ve formě nedeterministických konečných automatů syntetizovány na FPGA. Ačkoliv hardwarová akcelerace řeší rychlostní problémy, tak trpí zvýšenou spotřebou FPGA součástek, konkrétně LUT. Tato práce se zabývá návrhem, implementací a experimentálním vyhodnocením heuristické metody pro aproximaci konečných automatů pro rozpoznávání regulárních výrazů v hardware. Účelem této aproximace je snížení spotřeby LUT součástek při syntéze na FPGA. Princip redukční metody je založen na přidávání nových přechodů, čímž je zajištěna tvorba menšího počtu znakových tříd a je tak dosaženo zredukování spotřeby LUT při implementaci přechodů. Zavedená nepřesnost je minimalizována modifikací pouze méně významných částí automatu. Navržená metoda i s testovacím prostředím je implementována v nástroji TOFA. Technika byla vyhodnocena na syntetických i reálných datech. Výsledky experimentů ukázaly, že přechodová aproximace zvláště dobře funguje na automatech, kde se vyskytuje velký počet znakových tříd.
|
|
|
Automatický theorem prover
Mazánek, Martin ; Havlena, Vojtěch (oponent) ; Lengál, Ondřej (vedoucí práce)
Tato bakalářská práce se zabývá implementací systému pro automatické dokazování vět výrokové a predikátové logiky používajícím rezoluci. Cílem této práce je vytvořit jednoduchý systém a zdokumentovat jeho vývoj, nikoliv tvorba konkurenceschopného systému. Dále je v práci představeno několik populárních systémů automatického dokazování.
|
|
|
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.
|
host ::
RSS.