|
|
Beat Grep with Counters, Challenge
Horký, Michal ; Češka, Milan (referee) ; Holík, Lukáš (advisor)
Vyhledávání regulárních výrazů má ve vývoji softwaru nezastupitelné místo. Rychlost vyhledávání může ovlivnit použitelnost softwaru, a proto je na ni kladen velký důraz. Pro určité druhy regulárních výrazů mají standardní přístupy pro vyhledávání vysokou složitost. Kvůli tomu jsou náchylné k útokům založeným na vysoké náročnosti vyhledávání regulárních výrazů (takzvané ReDoS útoky). Regulární výrazy s omezeným opakováním, které se v praxi často vyskytují, jsou jedním z těchto druhů. Efektivní reprezentace a rychlé vyhledávání těchto regulárních výrazů je možné s použítím automatu s čítači. V této práci představujeme implementaci vyhledávání regulárních výrazů založeném na automatech s čítači v C++. Vyhledávání je implementováno v rámci RE2, rychlé moderní knihovny pro vyhledávání regulárních výrazů. V práci jsme provedli experimenty na v praxi používaných regulárních výrazech. Výsledky experimentů ukázaly, že implementace v rámci nástroje RE2 je rychleší než původní implementace v jazyce C#.
|
|
|
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.
|
|
|
Living in the suburbs
Holík, Lukáš ; Klimecký, Martin (referee) ; Gerö, Jiří (advisor) ; Pěnčík, Jan (advisor)
The aim of this bachelor's thesis was to create a low-energy / passive building located on the suburbs of the city Brno and which would serve for permanent housing. The land on which the building is to be located is currently mostly green. The ratio of the green area did not change from a bird's eye view, it only moved to other height levels. The majority of the proposed area is therefore greenery, in the form of green roofs. The resulting design consists of two two-storey buildings, which are separated by a green roof of garages located below ground level. However, it is one complex building, in which there are a total of 8 independent housing units of various sizes with gardens and terraces. The southern sides of the facades of both buildings form mainly glazed areas facing the gardens of the individual housing units. At the same time, large glass areas use as much southern light as possible, as both eastern and western in the design cannot be sufficiently used. This bachelor's thesis is based on the subject of studio work from the second year.
|
|
|
Development of Dataster Tool
Vlach, Martin ; Holík, Lukáš (referee) ; Smrčka, Aleš (advisor)
This bachelor thesis deals with expansion of existing web application Dataster in Testos platform. This application serves as a user interface for dbgenx tool from the same platform. The main purpose of Dataster is a user-friendly generation of randomized structured data which are used as a database test content. The first goal of this bachelor thesis was, in particular, to extend dbgenx tool with the possibility of generating test data according to the coverage criteria of combinatorial testing. An existing tool Combine from Testos platform has been selected for this purpose. The other part of the thesis deals with a number of small adjustments and expansion of Dataster web application, for a improvement of usability and overall user-friendliness of this application.
|
|
|
A Library for Binary Decision Diagrams
Paulovčák, Martin ; Holík, Lukáš (referee) ; Lengál, Ondřej (advisor)
The aim of this thesis is to create an easy-to-use library that will provide the basic means for Boolean function manipulation based on six different variants of Binary Decision Diagrams - BDD, ZDD, CBDD, CZDD, TBDD, and ESRBDD. The library is implemented in the ISO C programming language, uses closed hashing, index-based node referencing, mark and sweep based garbage collector and diagram construction is based on classical depth-first traversal. The implemented variants of these diagrams were compared on benchmarks and although the optimal choice of decision diagram variant depends on given problem, in general TBDD proved to be the best choice in terms of the resulting graph size and also CPU time.
|
|
|
Efficient Algorithms for Counting Automata
Mikšaník, David ; Holík, Lukáš (referee) ; Lengál, Ondřej (advisor)
Čítací automaty (CA) jsou klasické konečné automaty rozšířené o omezené čítače. CA stále reprezentují třídu regulárních jazyků, ale kompaktněji než konečné automaty. Jelikož jsou CA nedávným modelem, chybějí zde efektivní algoritmy implementující různé operace nad nimi. V této práci se primárně soustředíme na existující podtřídu CA zvanou monadické čítací automaty (MCA). Jsou to CA s čítacími smyčkami na třídě znaků, které se často vyskytují v praxi (např. při detekci paketů v síťovém provozu nebo analýze log souborů). Pro tuto podtřídu efektivně vyřešíme problémy prázdnosti a inkluze. Navíc poskytneme dvě rozšíření třídy MCA, které jsou stále podtřídou CA, a vyřešíme pro ně efektivně problém prázdnosti. MCA přirozeně vznikají z regulárních výrazů, které jsou rozšířené o čítací operátory vyskytující se pouze na třídě znaků. Náš algoritmus řešící problém inkluze MCA tedy může být použit jako základ nové metody pro testování inkluze takových regulárních výrazů. Tento přístup jsme experimentálně vyhodnotili na regulárních výrazech z praxe a porovnali s naivní metodou. Experimenty ukazují, že metoda používající náš algoritmus je více odolná proti stavové explozi. Také překonává naivní metodu, pokud regulární výrazy obsahují čítací operátory s velkými mezemi. Podle očekávání, pro jednoduché případy je naivní metoda stále rychlejší než metoda používající náš algoritmus.
|
|
|
Static Analysis in the Frama-C Environment Focused on Deadlock Detection
Dacík, Tomáš ; Holík, Lukáš (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zabývá návrhem nového statického analyzátoru pro detekci uváznutí, implementovaného jako plugin platformy Frama-C. Kromě samotného algoritmu pro detekci uváznutí představuje také odlehčené řešení, které umožňuje využít platformu Frama-C pro analýzu vícevláknových programů s využitím analyzátorů Frama-C podporujících pouze sekvenční programy. Výsledky experimentů ukazují, že implementovaný nástroj je schopný analyzovat reálné programy s vysokou přesností. Pro demonstraci další rozšiřitelnosti je představeno experimentální rozšíření umožňující detekovat také časově závislé chyby nad daty.
|
|
|
Efficient Algorithms for Finite Automata
Polanský, Ondřej ; Lengál, Ondřej (referee) ; Holík, Lukáš (advisor)
This thesis compares languages C++, C#, OCaml and Python based on speed, memory requirements and programming comfort. The goal of this thesis is to find out how much does the choice of a certain programming language impact the performance of programs working with finite automata. The same set of basic and advanced automata algorithms was implemented in each language and their efficiency was measured on a sample of 200 finite automata using a unix based operating system. Finally, the author presents results and discusses suitability of each language for work with finite automata. This thesis can help with selecting an appropriate programming language for multitude of purposes, including development of automata algorithm libraries or the process of designing programs and prototypes that work with finite automata.
|
|
|
Translation of LTL with Bounded Repetition to Automata with Counters
Slezáková, Alexandra ; Smrčka, Aleš (referee) ; Holík, Lukáš (advisor)
This work solves translation of LTL with bounded repetition (temporal operators that have limited validity for a certain number of steps) to automaton with counters. Using classical methods, the automaton representation of such formulas is large, because the size of automaton may be exponential to the upper limit of the bounded repetition. We present a construction that creates the automaton independent from repetition. The work represents a solution to the problem using the Büchi automaton with counters. The counters ensure that similar states and transitions are not created, which leads to a reduction in the size of the automaton. Our method is implemented and experimentally verified. We reduce the number of states of the automaton for formulas with large bound of operators several times in comparison to classical methods.
|
|
|
Efficient Algorithms for Büchi Automata
Laščák, Tomáš ; Holík, Lukáš (referee) ; Lengál, Ondřej (advisor)
The main goal of this work is to extend the existing library VATA with a module for working with Büchi automata, which are finite state automata over infinite words. These automata are used in many areas of computer science, among others in formal verifications, namely in LTL model checking. LTL model checking is typically carried out using the operation of testing language inclusion between two Büchi automata. Because testing language inclusion can be computationally very demanding, several optimized algorithms have been created for testing language inclusion such as the Ramsey-based approach. This work is focused on the mentioned approach, the implementation of which is added to the newly created extension of the VATA library. Apart from that, the new extension adds additional useful operations over Büchi automata such as union, intersection or a reduction in the number of states.
|
guest ::
RSS feed.