|
|
Improvements of the ASMA Tool for Analysis of String Manipulating Programs via Symbolic Automata
Kmenta, Martin ; Lengál, Ondřej (oponent) ; Vojnar, Tomáš (vedoucí práce)
In this work we deal with regular model checking which is a technique for analyzing programs whose state space can be infinite due to dealing with, e.g. unbounded queues, parameters, dynamically linked data structures, recursive procedures, or strings. The goal of this work was to implement improvements to the existing prototype tool ASMA implementing regular model checking over the Microsoft Automata library. We analysed the source code of ASMA and reran analyses of all available benchmark programs. We identified some bottlenecks and have tackled several of them. In particular, we integrated a library containing additional reduction algorithms into ASMA, created several new versions of the reverse concatenation operation, which tuned out to be very costly in the benchmarks, improved the command line interface of ASMA, and implemented some other optimizations for ASMA. The computation time was reduced by 90 % when analysing bigger programs.
|
|
|
Mnohaúrovňové automaty a jejich aplikace
Pšenák, Kamil ; Tomko, Martin (oponent) ; Meduna, Alexandr (vedoucí práce)
V tejto práci rozšírime zastarané prístupy v teoretickej informatike. Ukážeme si, že je možný paralelizmus v konečných automatoch zavedením viacúrovňového konceptu. Priblížime si proces kompilácie a stavbu kompilátoru, aby sme mali reálny príklad pre viacúrovňové konečné automaty. Posunieme sa hlbšie do teoretickej informatiky a vysvetlíme si paralelné pravo-lineárne gramatiky a jazyky. Následne si na príklade aj s návrhom implementácie dokážeme tvrdenie. Na záver si spomenieme ďalšie možné odvetvia, kde by sa tento koncept dal využiť.
|
|
|
Srovnání efektivity různých programovacích jazyků při práci s automaty
Polanský, Ondřej ; Lengál, Ondřej (oponent) ; Holík, Lukáš (vedoucí práce)
V této práci jsou srovnány jazyky C++, C#, OCaml a Python na základě rychlosti, paměťové náročnosti a programátorské přívětivosti. Práce si klade otázku, jak moc se liší programy pracující s konečnými automaty, pokud jsou zapsané v různých jazycích. V každém jazyce je implementována stejná sada základních a pokročilých automatových algoritmů a následně je měřena jejich efektivita na vzorku 200 konečných automatů na unixovém operačním systému. Závěrem jsou prezentovány výsledky a je diskutována vhodnost jednotlivých jazyků pro práci s automaty. Tato práce může posloužit například při výběru jazyka pro tvorbu knihoven pro práci s automaty nebo při návrhu programů a prototypů algoritmů pracujících s automaty.
|
|
|
Strojové učení pro odvozování modelů formálních jazyků
Bardonek, Petr ; Kocman, Radim (oponent) ; Křivka, Zbyněk (vedoucí práce)
Tato bakalářská práce se zabývá odvozováním modelů formálních jazyků. Jedná se o vědní disciplínu na poli výzkumu umělé inteligence. Cílem je vytvořit aplikaci umožňující automatické vytvoření modelu, v podobě konečného automatu, pro neznámý formální jazyk na základě množiny řetězců neznámého formálního jazyka s využitím upravené metody strojového učení.
|
|
|
Efektivní algoritmy pro konečné automaty
Kantor, Tomáš ; Rogalewicz, Adam (oponent) ; Lengál, Ondřej (vedoucí práce)
Tato práce prezentuje nový algoritmus pro komplementaci nedeterministických konečných automatů. Současné metody vyžadují převod na deterministický konečný automat, který může mít exponenciálně větší počet stavů. Navržený algoritmus pracuje iterativně po jednotlivých silně souvislých komponentách konečného automatu. Díky tomu umožňuje jednotlivé části efektivněji komplementovat, redukovat a následně propojit s ostatními částmi automatu. Tento algoritmus je tak efektivnější než současné metody pro určité typy konečných automatů.
|
|
|
Detekce narušení počítačové sítě
Hank, Andrej ; Martínek, Tomáš (oponent) ; Kořenek, Jan (vedoucí práce)
Stále rastúce rozšírenie a priepustnosť počitačových sietí prináša mnoho bezpečnostných hrozieb. Jedným z prostriedkov zabezpečenia sú systémy detekcie narušenia (IDS). Nízka priepustnosť softwérových IDS vyúsťuje vo vývoj hardwérových akcelerátorov. Konkrétnym je sonda Traffic Scanner projektu Liberouter využívajúca technológiu FPGA. Jadro akcelerácie spočíva vo vyhľadávaní jednoduchých reťazcov v obsahu paketu. Komplexný popis reťazcov zaručujú regulárne výrazy. Táto práca obohacuje sondu Traffic Scanner o možnosť pokročilého vyhľadávania reťazcov pomocou Perl Compatible Regular Expressions (PCRE) implementovaným transformátorom. Ďalej prináša návrh a implementáciu programového vybavenia umožňujúceho využiť funkcionalitu akcelerátoru užívateľom. Podáva koncepciu detekcie narušenia sieťe s využítím sondy Traffic Scanner a možnosti spolupráce s inými bezpečnostnými zariadeniami.
|
|
|
Multidimensionální jazyky a jejich automaty
Dibďák, Lukáš ; Martiško, Jakub (oponent) ; Meduna, Alexandr (vedoucí práce)
Práce seznamuje s teorií formálních jazyků a konečných automatů. Popisuje zobecnění této teorie do dvou rozměrů. Představuje základní typy dvoudimensionálních automatů, přede- vším teselační automaty. Pro teselační automaty jsou nabídnuty algoritmy k jejich determinizaci. Jeden z algoritmů je následně používán přiloženou aplikací pro determinizaci.
|
|
|
Implementace jednotky pro vyhledávání vzorů v FPGA
Košař, Vlastimil ; Kořenek, Jan (oponent) ; Kaštil, Jan (vedoucí práce)
Tato práce pojednává o algoritmech pro vyhledávání vzorů používaných v moderních systémech pro detekci nežádoucího provozu, přičemž se zaměřuje na algoritmy umožňující vyhledávání regulárních výrazů. Zabývá se přístupy založenými na deterministických a nedeterministických konečných automatech, hybridními přístupy a přístupem založeným na regulárních výrazech jako programovacím jazyku speciálních procesorů. Dále popisuje návrh implementace jednotek pro vyhledávání vzorů popsaných regulárními výrazy založených na několika z popsaných přístupů včetně metodiky odhadu zabraných zdrojů. V další části je popsán vyvinutý softwarový systém pro generování jednotek. V následující části jsou ukázány a diskutovány dosažené výsledky.
|
|
|
A Library for Computing Simulation Relations over Büchi Automata
Odvárka, Daniel ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
This thesis presents the topic of simulation relations over Büchi automata and the use case of various simulations. The simulation relations are important for reducing a state space of an automaton, or checking the under approximation of language inclusion. There are also parity games, which are important for computing some of the simulation types we introduce. We will go over multiple algorithms that compute these simulation relations. The mentioned algorithms are implemented in programming language C++ and are compared to a tool named RABIT. Our implementation is better only for smaller sized automata.
|
|
| |
host ::
RSS.