|
|
Next Generation of Rank-Based Algorithms for Omega Automata
Šmahlíková, Barbora ; Holík, Lukáš (referee) ; Lengál, Ondřej (advisor)
Komplementace Büchiho automatů je klíčovou operací pro terminační analýzu programů, model checking nebo rozhodovací procedury pro různé logiky. Tato práce se zabývá především optimalizacemi rank-based komplementace Büchiho automatů. Původní rank-based algoritmus je sice asymptoticky optimální, přesto může generovat nezbytně velký stavový prostor. Pro praktické použití je tedy žádoucí maximálně redukovat počet vygenerovaných stavů v komplementu. V této práci představíme několik technik pro efektivní komplementaci některých speciálních typů Büchiho automatů, často se vyskytujících v praxi, které jsou založené na jejich struktuře. Některé z navržených technik lze do určité míry rozšířit i pro obecné Büchiho automaty. Techniky představené v této práci byly implementovány jako rozšíření nástroje Ranker pro komplementaci Büchiho automatů. Tyto optimalizace výrazně redukují generovaný stavový prostor a Ranker ve většině případů produkuje menší komplement než ostatní existující nástroje pro komplementaci.
|
|
|
An Efficient Functional Library for Finite Automata
Říha, Jakub ; Hruška, Martin (referee) ; Lengál, Ondřej (advisor)
Finite automata are an important mathematical abstraction, and in formal verification, they are used for a concise representation of regular languages. Operations often used on finite automata in this setting are testing their universality and language inclusion. \mbox{A naive} approach to implement these operations leads to an explicit determinization of the automata, which can be costly and undesirable. There is, however, a more advanced method for performing those operations, called the Antichains algorithm, which avoids such an explicit determinization. This work shows how finite automata operations can be effectively implemented in Haskell and compares several approaches of their implementation. The obtained results are compared with VATA, an imperative implementation of a finite automata library.
|
|
|
Efficient Algorithms for Tree Automata
Valeš, Ondřej ; Hruška, Martin (referee) ; Lengál, Ondřej (advisor)
In this work a novel algorithm for testing language equivalence and inclusion on tree automata is proposed and implemented as a module in the VATA library. First, existing approaches to equivalence and inclusion testing on both word and tree automata are examined. These existing approaches are then modified to create bisimulation up-to congruence algorithm for tree automata and a formal proof of the soundness of the new algorithm is provided. Efficiency of this new approach is compared with existing language equivalence and inclusion testing methods for tree automata, showing the performance of our algorithm on hard cases is often superior.
|
|
|
Functional Verification of Processor Execution Units
Valach, Lukáš ; Lengál, Ondřej (referee) ; Masařík, Karel (advisor)
The thesis deals with integration of functional verification into the design cycle of execution units in a hardware-software co-design environment of the Codasip system. The aim of the thesis is to design and implement a verification environment in SystemVerilog in order to verify automatically generated hardware representation of the execution units. In the introduction, advantages and basic methods of functional verification and principles of the Codasip system are discussed. Next chapters describe the process of design and implementation of the verification environment of arithmetic-logic unit as well as the analysis of the results of verification. In the end, a review of accomplished goals and the suggestions for future development of the verification environment are made.
|
|
|
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.
|
|
|
Event-Driven Automation
Havlín, Jan ; Češka, Milan (referee) ; Lengál, Ondřej (advisor)
The thesis deals with automation of processes in Testing Farm Team of company Red Hat Czech s.r.o. Automating the chosen task "Update and test continuous integration system with new operating system build results in simplified maintenance of said continuous integration system. Implementation uses a Jenkins server to execute jobs and tft-admin tool to perform smaller steps resulting in automation of the task. Also, in the implementation part, modifications of the tft-admin tool allow usage in automated scripts which simplifies future automation of other processes.
|
|
|
Controlling Autonomous Systems Based on Partially Observable Markov Decision Processes
Gyselová, Julie ; Lengál, Ondřej (referee) ; Češka, Milan (advisor)
Systémy se stavovou neurčitostí lze modelovat pomocí Markovských rozhodovacích procesů s částečným pozorováním. Agent, který se v takovém systému pohybuje, má o své pozici v rámci systému pouze omezené informace (pozorování). Konečně-stavový kontroler umí přiřadit vhodnou akci k aktuálnímu pozorování. Díky tomu může agent se systémem lépe interagovat a dobrat se svého cíle. Nástroj PAYNT umí najít nejkvalitnější kontroler mezi všemi možnými kontrolery dané velikosti pro daný model. V této práci představím způsob, jakým lze omezit designový prostor, ve kterém PAYNT kontrolery hledá, tak, aby zakódovával pouze určitou podmnožinu kontrolerů, která lze vyhodnotit v menším čase. Pokud je použita vhodná restrikce, kvalita kontrolerů není ovlivněna. Dále implementuji metodu, která postupně aplikuje tyto restrikce na designový prostor a umožňuje syntetizační metodě v PAYNTu nepřetržitě hledat kontrolery větších velikostí a lepší kvality.
|
|
|
A Verified Data Structures Library
Rychnovský, Jan ; Holík, Lukáš (referee) ; Lengál, Ondřej (advisor)
This bachelor thesis deals with a methodology of writing verified programs using the VCC tool. The mentioned methodology is based in the principle of extending the program code with additional annotations, which provide a specification of the desired functionality. The VCC tool then uses formal methods to check whether the source code is correct with respect to the given specification. The first part describes formal verification and three basic approaches to it. Subsequently, the satisfiability problems of propositional formulae (SAT) and formulae in theories of predicate logic (SMT) are described. Then the thesis describes the VCC verification tool, its functionality, methodology, syntax and semantics of commands of its intermediate annotation language BoogiePL. The second part of this thesis is focused on the design and implementation of a verified data structures library, which contains singly linked, doubly linked, and circular lists, a binary search tree and a Treiber's stack. The text concludes with a discussion of the learnt knowledge about the programming methodology based on writing verified code.
|
|
|
Infrastructure for Testing and Deployment in the Field of Containers
Ormandy, Adam ; Lengál, Ondřej (referee) ; Turoňová, Lenka (advisor)
Znížená efektivita spôsobená robením repetitívnych a manuálnych prác je častým problémom v IT. Vývojári často testujú a nasadzujú svoj software manuálne, čo je nielen náročné na čas, nezáživné a náchylné k chybám. Táto práca sa snaží v rámci jedného DevOps tímu, vyriešiť tento problém pomocou zjednotenia vývojárskych a testovacích nástrojov, a pomocou aplikovania pricípov CI a CD do produkčného prostredia. Zároveň sa sústredí na software využívajúci Python, Jenkins a kontajnery. Hlavnými použitými nástrojmi sú GitLab CI, OpenShift a Tox. Vďaka tejto práci sa podarilo zvýšit počet projektov, ktoré používajú CI/CD zo 7 na 50 percent, zvrátiť rastúci trend v počte porušení štýlu v jazyku Python, opatriť kontajnery metadátami, zautomatizovať proces tvorby kontajnerov, ušetriť čas nerobením repetitívnych úloh a pod.
|
|
|
A Web Interface for the Management of Virtual Portfolio
Bali, Filip ; Hruška, Martin (referee) ; Lengál, Ondřej (advisor)
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.
|
guest ::
