|
|
Cluster Data Visualization for InfiSpector
Hais, Vratislav ; Lengál, Ondřej (oponent) ; Šimková, Hana (vedoucí práce)
This bachelor's thesis is focused on InfiSpector data visualization by adding a new graph used as a time selector and by modifying open source diagrams that are designed to fit InfiSpector needs. Theory about general data visualization, description of the InfiSpector tool and libraries used mainly for data visualization are described in the beginning. Next, our customized solution and already existing solutions are also described. Finally, last part evaluate accomplished results and propose possible improvements.
|
|
|
Server for Continuous Integration
Šajdík, Michal ; Fiedor, Tomáš (oponent) ; Lengál, Ondřej (vedoucí práce)
This work contains description about the following topics: what kind of technologies and principles are needed for creation of a continuous integration server, already existing solutions, why there is a need to create a new one, and how to integrate continuous integration server which was created during this work, based on the information mentioned in this work, to a working environment. This work also shows effects and some side effects of correct and incorrect configuration of the mentioned continuous integration server. Mentioned continuous integration server is also able to run on MS Windows 10 and Linux without need to adapt a configuration for a specific operating system.
|
|
|
Abstraction in Automata Algorithms
Kocourek, Tomáš ; Lengál, Ondřej (oponent) ; Holík, Lukáš (vedoucí práce)
The goal of this thesis is to implement and experimentally compare antichain-based algorithms with and without abstraction, which decide the emptiness of alternating finite automata. The author also proposes his own algorithms using abstraction and comes up with a few optimizations of existing abstract algorithms. The thesis introduces the theoretical background of studied algorithms and describes efficient ways to implement data structures which are used by these algorithms. The experimental evaluation over random automata shows that the algorithms without abstraction give us better results in general because they do not perform costly evaluation of closed set intersection and complementation. However, in case of automata with high transition density, the algorithms without abstraction tend to decelerate, while the abstract ones accelerate.
|
|
|
Webová aplikace pro správu elektronické knihovny
Kocman, Radim ; Rogalewicz, Adam (oponent) ; Lengál, Ondřej (vedoucí práce)
Cílem této práce je vytvoření webové aplikace pro správu elektronické knihovny, která vytváří webové rozhraní nad programem Calibre. Při tvorbě bylo dbáno na to, aby byl výsledek dále jednoduše rozšiřitelný a přístupný širokému okruhu uživatelů. Základem systému je jazyk PHP a knihovna Nette Framework. Text této práce popisuje kompletní vývojový cyklus aplikace od rozboru současného stavu přes analýzu požadavků, návrh systému a návrh uživatelského rozhraní až po implementační detaily a rozbor testování na vzorku uživatelů.
|
|
|
Automata in Infinite-state Formal Verification
Lengál, Ondřej ; Jančar, Petr (oponent) ; Veith, Helmut (oponent) ; Esparza, Javier (oponent) ; Vojnar, Tomáš (vedoucí práce)
The work presented in this thesis focuses on finite state automata over finite words and finite trees, and the use of such automata in formal verification of infinite-state systems. First, we focus on extensions of a previously introduced framework for verifi cation of heap-manipulating programs-in particular programs with complex dynamic data structures-based on tree automata. We propose several extensions to the framework, such as making it fully automated or extending it to consider ordering over data values. Further, we also propose novel decision procedures for two logics that are often used in formal verification: separation logic and weak monadic second order logic of one successor. These decision procedures are based on a translation of the problem into the domain of automata and subsequent manipulation in the target domain. Finally, we have also developed new approaches for efficient manipulation with tree automata, mainly for testing language inclusion and for handling automata with large alphabets, and implemented them in a library for general use. The developed algorithms are used as the key technology to make the above mentioned techniques feasible in practice.
|
|
|
Vizualizace datových struktur pro verifikační nástroje
Holubec, Michael ; Lengál, Ondřej (oponent) ; Peringer, Petr (vedoucí práce)
Cílem práce je objektově orientovaný návrh a implementace knihovny, která poskytne verifikačnímu nástroji Predator a dalším nástrojům jednotné rozhraní pro vizualizaci interních datových struktur především pro účely jejich ladění. Práce analyzuje některé vlastnosti verifikačních nástrojů Predator, Forester a CPAchecker. Knihovna poskytuje nejen grafický, ale také textový výstup ve formátu jazyka DOT. Výsledek byl otestován připojením knihovny k verifikačnímu nástroji Predator.
|
|
|
Nástroj pro statickou analýzu programů se seznamy
Kotoun, Michal ; Lengál, Ondřej (oponent) ; Vojnar, Tomáš (vedoucí práce)
Tvorba softwarového analyzátoru je komplexní úloha -- je nutno implementovat parsování zdrojového kódu, reprezentaci instrukcí, abstrakci hodnot, uživatelské rozhraní, ... a také analýzu samu. Abychom předešli zbytečné práci vývojářů analýz, rozhodli jsme se vytvořit framework pro statickou analýzu programů. Předkládáme obecný návrh frameworku zvaného Angie s důrazem na jeho použitelnost a popisujeme prototyp frameworku, včetně modelové analýzy založené na symbolických paměťových grafech. Angie je implementován v C++ a používá nástroje z kolekce LLVM pro parsování zdrojového kódu analyzovaných programů.
|
|
|
Efficient Algorithms for Counting Automata
Mikšaník, David ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
Counting automata (CAs) are classical finite automata extended with bounded counters. They still denote the class of regular languages but in a more compact way than finite automata. Since CAs are a recent model, there is a gap in the knowledge of efficient algorithms implementing various operations on the CAs. In this thesis, we mainly focus on an existing subclass of CAs called monadic counting automata (MCAs), i.e., CAs with counting loops on character classes, which are common in practice (e.g., detection of packets in network traffic, log analysis). For this subclass, we efficiently solve the emptiness and inclusion problems. Moreover, we provide two extensions of the class of MCAs (but not beyond the class of CAs) and efficiently solve the emptiness problem for them. MCAs naturally arise from regular expressions that are extended by the counting operator limited only to character classes. Thus our algorithm solving the inclusion problem of MCAs can be used in a new method for solving the inclusion problem of such regular expressions. We experimentally evaluated this method on regular expressions from a wide range of applications and compared it with the naive method. The experiments show that the method using our algorithm is less prone the explode. It also outperforms the naive method if the regular expressions contain counting operators with large bounds. As expected, for the easy cases, the naive method is still faster than the method based on our algorithm.
|
|
|
Efektivní algoritmy pro práci s konečnými automaty
Hruška, Martin ; Rogalewicz, Adam (oponent) ; Lengál, Ondřej (vedoucí práce)
Nedeterministické konečné automaty jsou používány v mnoha oblastech informatiky, mimo jiné také ve formální verifikaci, při návrhu číslicových obvodů nebo pro reprezentaci regulárlních jazyků. Jejich výhodou oproti deterministickým konečným automatům je schopnost až exponenciálně stručnější reprezentace jazyka. Nicméně, tato výhoda může být pozbyta, jestliže je zvolen naivní přístup k implementaci některých operací, jako je na\-pří\-klad test jazykové inkluze dvojice automatů, jehož naivní implementace provádí explicitní determinizaci jednoho z automatů. V nedávné době bylo ale představeno několik nových přístupů, které právě explicitní determinizaci při testu jazykové inkluze předcházejí. Tyto přístupy využívají tzv. antichainů nebo tzv. bisimulace vzhůru ke kongruenci. Cílém této práce je vytvoření efektivní implementace zmíněných přístupů v podobě nového rozšíření knihovny VATA. Vytvořená implementace byla otestována a je až řádově rychlejší v 90% testovaných případů nežli implementace jiné
|
|
|
Překladač grafu toků dat do logiky bitových vektorů
Sušovský, Tomáš ; Lengál, Ondřej (oponent) ; Smrčka, Aleš (vedoucí práce)
Cílem této bakalářské práce je vytvořit a implementovat nástroj pro překlad modelů grafů toků dat do formátu SMT-LIB. Práce navazuje na projekt HADES výzkumné skupiny VeriFIT Fakulty informačních technologií Vysokého učení technického v Brně. V řešení bylo použito překladače vytvářejícího z původního grafu objektový model. Objektový model je možné převést do zápisu ve formátu SMT-LIB a přidat do něj aserce požadovaných vlastností systému. Pro ověřování vlastností závisejících na změnách systému je použita metoda rozbalování smyček s uživatelem zadanou hranicí maximálního počtu rozbalení. Možnosti vytvořeného nástoje jsou demonstrovány na sadě modelů grafů toků dat pokrývající všechny prvky vstupního jazyka VAM a jejich kombinace. Výsledek této práce představuje nové možnosti pro zpracování grafů toků dat ve formátu VAM a jejich verifikaci.
|
host ::
RSS.