|
|
Next Generation of Rank-Based Algorithms for Omega Automata
Šmahlíková, Barbora ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
Büchi automata (BA) complementation is a crucial operation for termination analysis of programs, model checking, or decision procedures for various logics. Despite its prominence, practically efficient algorithms for BA complementation are still missing. This thesis deals with optimizations of Büchi automata complementation, focusing mainly on rank-based techniques. The original rank-based algorithm is asymptotically optimal, but it can still generate unnecessarily large state space. For a practical usage, it is therefore desirable to reduce the number of generated states in the complement as much as possible. We propose several techniques that can efficiently complement some special types of Büchi automata, occuring often in practice, based on their structure. Some of these techniques can also, to a certain degree, be extended to general Büchi automata. The developed techniques were implemented as an extension of the tool Ranker for Büchi automata complementation and evaluated on thousands of hard automata. Our optimizations significantly reduce the generated state space and Ranker produces in the majority of cases a~smaller complement than other state-of-the-art tools.
|
|
|
Efektivní funkcionální knihovna pro konečné automaty
Říha, Jakub ; Hruška, Martin (oponent) ; Lengál, Ondřej (vedoucí práce)
Konečné automaty jsou důležitou matematickou abstrakcí. Ve formální verifikaci se konečné automaty používají ke stručné reprezentaci regulárních jazyků. V této souvislosti se používají operace nad konečnými automaty, jako je testování jazykové univerzality a inkluze. Naivní přístup k implementaci těchto operací vede k explicitní determinizaci konečného automatu, což může být nakladné a nežádoucí. Nicméně existuje pokročilejší metoda k vykonávání těchto operací nazývaná Antichains algoritmus, která se vyhýbá explicitní determinizaci. Tato práce se zabývá efektivní implementací operací nad konečnými automaty v Haskellu a také porovnává několik implementačních variant. Získané výsledky jsou poté porovnány s knihovnou VATA, což je imperativní implementace knihovny pro práci nad konečnými automaty.
|
|
|
Efektivní algoritmy pro stromové automaty
Valeš, Ondřej ; Hruška, Martin (oponent) ; Lengál, Ondřej (vedoucí práce)
Cílem této práce je navržení efektivních algoritmů pro testování jazykové ekvivalence a inkluze stromových automatů a dále pak implementace těchto algoritmů jako rozšíření knihovny VATA. Nejprve je provedena rešerše existujících přístupů testování ekvivalence a inkluze slovních i stromových automatů. Z nich poté vychází návrh nového přístupu k testování ekvivalence a inkluze jazyků stromových automatů založený na bisimulaci vzhledem ke kongruenci, ke kterému je představen formální důkaz korektnosti. Součástí práce je také srovnání efektivity představeného algoritmu a již existujících přístupů, které ukazuje, že na obtížných případech je náš algoritmus často lepší než existující přístupy.
|
|
|
Funkční verifikace výpočetních jednotek procesoru
Valach, Lukáš ; Lengál, Ondřej (oponent) ; Masařík, Karel (vedoucí práce)
Práce se zaobírá začleněním procesu funkční verifikace do vývojového cyklu návrhu funkčních jednotek v prostředí pro souběžný návrh hardwaru a softwaru systému Codasip. Cílem bylo navrhnout a implementovat verifikační prostředí v jazyku SystemVerilog pro verifikaci automaticky generované hardwarové reprezentace těchto jednotek. Na začátku jsou rozebrány přínosy a obvyklé postupy při funkční verifikaci a vlastnosti systému Codasip. Dále je v práci popsán návrh, implementace, analýza průběhu a výsledků testů verifikace simulačního modelu aritmeticko-logické jednotky. Závěrem jsou zhodnoceny dosažené výsledky práce a navrhnuta zlepšení pro možný další rozvoj verifikačního prostředí.
|
|
|
A Library for Binary Decision Diagrams
Paulovčák, Martin ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
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.
|
|
|
Událostmi řízená automatizace
Havlín, Jan ; Češka, Milan (oponent) ; Lengál, Ondřej (vedoucí práce)
Práce se zabývá automatizací procesů v rámci týmu Testing Farm firmy Red Hat Czech s.r.o. Automatizací vybrané úlohy "Aktualizace a otestování systému průběžné integrace s novým sestavením operačního systému se docílilo snadnější údržby tohoto systému průběžné integrace. Implementace využívá Jenkins server ke spouštění úloh a nástroj tft-admin k vykonávání dílčích kroků vedoucích k automatizaci dané úlohy. Dále implementace umožňuje využití nástroje tft-admin k používání v automatizovaných skriptech, což do budoucna usnadňuje automatizaci dalších procesů.
|
|
|
Controlling Autonomous Systems Based on Partially Observable Markov Decision Processes
Gyselová, Julie ; Lengál, Ondřej (oponent) ; Češka, Milan (vedoucí práce)
Partially observable Markov decision processes offer a way to model systems with state uncertainty. An agent has limited information (observation) about its current location in the system. A finite-state controller that translates this information to actions that the agent can perform helps the agent interact with the model and achieve its goals. PAYNT is a tool that constructs a design space that contains all possible finite-state controllers of a given size for a POMDP and then tries to find the best FSC among those. In this thesis, I introduce a way to restrict the design space to encode only a subset of the controllers so that PAYNT can find the best controller in a much shorter time. If the used restriction is suitable, the controller quality is not affected. I also implement a method that can make the synthesis method implemented in PAYNT continuously find FSCs of increasing sizes and improving qualities by gradually applying restrictions from a predefined set.
|
|
|
Verifikovaná knihovna datových struktur
Rychnovský, Jan ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
Tato bakalářská práce se zabývá metodikou psaní verifikovaných programů pomocí nástroje VCC. Zmíněná metodika je založena na principu doplnění kódu programu o anotace, jež poskytují specifikaci požadované funkcionality. Nástroj VCC pak prostřednictvím formálních metod určí zda zdrojový kód splňuje danou specifikaci či ne. V první části práce je popsána formální verifikace a zmíněny tři základní přístupy k ní. Následně jsou popsány problémy splnitelnosti výrokových formulí (SAT) a splnitelnosti formulí v teoriích predikátové logiky (SMT). Práce se dále věnuje popisu verifikačního nástroje VCC, jeho funkčnosti, metodice, syntaxi a sémantice příkazů jeho anotačního jazyka BoogiePL. Druhá část textu je zaměřena na popis návrhu a implementace verifikované knihovny datových struktur obsahující jednosměrný, dvousměrný a kruhový seznam, binární vyhledávací strom a Treiberův zásobník. Závěr práce diskutuje získané poznatky o programovací metodice založené na psaní verifikovaného kódu.
|
|
|
Infrastructure for Testing and Deployment in the Field of Containers
Ormandy, Adam ; Lengál, Ondřej (oponent) ; Turoňová, Lenka (vedoucí práce)
Efficiency loss caused by repetitive manual tasks is a common problem throughout the IT sector. Developers often test, build, and deploy their software manually. That is not only time-consuming, but also dull and prone to errors and mistakes. This thesis tries to solve that in the context of one DevOps team, by unifying the development and testing tools, and by applying the principles of continuous integration and continuous deployment in the production environment. It is focused on Python, Jenkins, and container-based software and workflows. The main tools used in the thesis are GitLab CI, OpenShift and Tox. Thanks to work in described in the thesis, the number of projects with CI/CD pipelines increased from 7 to 50 percent, the amount of Python style violations started to decrease, containers have proper metadata, the container build process is automated, time and effort are saved by not doing repetitive tasks, and more.
|
|
|
A Web Interface for the Management of Virtual Portfolio
Bali, Filip ; Hruška, Martin (oponent) ; Lengál, Ondřej (vedoucí práce)
This thesis designs and implements a web application for managing virtual portfolios. Main goal of the application is visualise and analyze data from stock exchange services API. User can be notified on price change. The application also uses existing methods to predict stock prices and supports the visualization of the user's stock exchange decisions and provides him/her a general overview of them.
|
host ::
RSS.