|
|
Approximate Techniques for Markov Models
Andriushchenko, Roman ; Havlena, Vojtěch (referee) ; Češka, Milan (advisor)
In this work we discuss approximative techniques for the analysis of Markov chains, namely, state space aggregation and truncation. First, we focus on the application of the former method for the analysis of discrete-time models: we redesign the clustering algorithm to handle chains with an arbitrary structure of the state space and, most importantly, we improve upon existing bounds on the approximation error. The developed approach is then integrated with uniformisation techniques, in both standard and adaptive forms, to approximate continuous-time models as well as provide estimates of the approximation error. This theoretical framework along with existing truncation-based techniques were implemented within PRISM model checker. Experiments confirm that newly derived bounds provide a several orders of magnitude precision improvement without degrading performance. We show that the resulting aggregating approach can provide a valid model approximation supplied by adequate approximation error estimates, in both discrete and continuous time. Then, we perform a comparative analysis of aggregating and truncating techniques, illustrate how different methods handle various types of models, and identify chains for which aggregating, or truncating, analysis is preferred. Finally, we demonstrate a successful usage of approximative techniques for model checking Markov chains.
|
|
|
Synthesis of Probabilistic Programs with Rewards
Hranička, Vojtěch ; Síč, Juraj (referee) ; Češka, Milan (advisor)
This thesis pursues the synthesis of probabilistic programs with rewards. Probabilistic synthesis leads to the automatic proposal of a system which fulfills required specifications. In this thesis, I work with a form of synthesis where we have a sketch of a given system. This sketch includes unknown variables and the objective is to find a combination of configuration of given variables in order to have the final program meeting the specified requirements. Recently, new approaches considering a set of solutions as a family of Markov chain have appeared. One of these approaches is the usage of a new method combining counterexample-guided abstraction refinement and counterexample-guided inductive synthesis. This method exceeds other methods for synthesis of probabilistic programs with its efficiency. In this thesis, I concretely focus on extending this tool's specification language by adding a possibility of application of rewards and until properties. Thanks to these extensions it is possible to specify searched solution more efficiently. Experiments demonstrate that even after the addition of these possibilities of specifications the speed of a given tool remains by a margin of order of magnitudes more effective than the standard method of synthesis.
|
|
|
GPU-Accelerated Synthesis of Probabilistic Programs
Marcin, Vladimír ; Matyáš, Jiří (referee) ; Češka, Milan (advisor)
V tejto práci sa zoberáme problémom automatizovanej syntézy pravdepodobnostných programov: majme konečnú rodinu kandidátnych programov, v ktorej chceme efektívne identifikovať program spĺňajúci danú špecifikáciu. Aj riešenie tých najjednoduchších syntéznych problémov v praxi predstavuje NP-ťažký problém. Pokrok v tejto oblasti prináša nástroj Paynt, ktorý na riešenie tohto problému používa novú integrovanú metódu syntézy pravdepodobnostných programov. Aj keď sa tento prístup dokáže efektívne vysporiadať s exponenciálnym rastom rodín kandidátnych riešení, stále tu existuje problém spôsobený exponenciálnym rastom jednotlivých členov týchto rodín. S cieľom vysporiadať sa aj s týmto problémom, sme implementovali GPU orientované algoritmy slúžiace na overovanie kandidátnych programov (modelov), ktoré danú úlohu paralelizujú na stavovej úrovni pravdepodobnostých modelov. Celkové zrýchlenie doshiahnuté týmto prístupom za určitých podmienok potom prinieslo takmer teoretický limit možného zrýchlenia syntézneho procesu.
|
|
|
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#.
|
|
|
An Extension of the ANaConDa Tool for Dynamic Analysis of Concurrent Programs
Horňák, Michal ; Češka, Milan (referee) ; Vojnar, Tomáš (advisor)
The main goal of this thesis is to implement algorithm FastTrack for dynamic analysis of multi-threaded programs in C/C++. FastTrack is algorithm which detects data race errors. It is based on happens-before relation encoded into the vector-clocks.Vector-clocks allows extrapolation of the execution which improves detection of potential errors, which were not seen in the actual run of the program however in other executions they could cause problems. Algorithm is implemented into the framework ANaConDA. ANaConDA is a tool for implementation of dynamic analyzers of parallel programs on binary level. It provides neccessary run time program informations for detectors use to discover concurency errors.
|
|
|
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 Tool for Building CEG Graphs
Mutňanský, Filip ; Češka, Milan (referee) ; Smrčka, Aleš (advisor)
Cause-effect graphing is one of approaches to requirement-based testing. Cause-effect graphs (CEG) are used to visualize logic relations among requirements and to fill in a decision table to form test cases. The goal of this bachelor's thesis is to design and implement a tool for creating and manipulating with CEG graphs. The developed tool is implemented as a single-page web application. The manipulation with CEG is possible via graphical user interface and/or via text-based specification in a CEG specific language. Moreover, the tool uses logic solver to ease a user with creation of the decision table.
|
|
|
An Automata-Based Decision Procedure
Hečko, Michal ; Češka, Milan (referee) ; Lengál, Ondřej (advisor)
Presburgerova aritmetika (PrA) je rozhodnutelná teorie přirozených čísel prvního řádu, která nachází uplatnění v mnoha oblastech formální verifikace vlastností softwaru. Řešiče SMT nástroje implementující různé algoritmické přístupy k rozhodování, zda má formule řešení hrají ve formální verifikaci klíčovou roli. V této práci dokumentujeme vytvoření nového automatického SMT řešiče pro PrA založeného na konečných automatech přístupu, který v současnosti žádný SMT řešič nepoužívá. Uvádíme přehled výzev a jejich řešení vyplývajících ze složitosti takového nástroje, včetně výsledků z provedených experimentů, které již identifikují problémy, kde tento alternativní přístup překonává nejmodernější řešiče. Uvádíme také identifikované problémy, u nichž výkonnost postupu založeného na automatech naráží na problémy, které představují otevřené možnosti výzkumu.
|
|
|
Visualising CPU Activity
Ďurčo, Marián ; Češka, Milan (referee) ; Vojnar, Tomáš (advisor)
This thesis is intended to be a complement for learning about the RISC pipeline. Product of this thesis is a web application. After reviewing various tools and libraries suitable for this work, we have chosen two main libraries React and Redux. The created solution allows the instruction flow to be displayed in the RISC pipeline as well as states of the registers and the memory. It makes easy to perform transitions between the various parts of the visualization. This visualization allows a basic understanding of the RISC pipeline principles and also individual assembly instructions.
|
guest ::
RSS feed.