|
|
Aproximativní techniky pro Markovovy modely
Andriushchenko, Roman ; Havlena, Vojtěch (oponent) ; Češka, Milan (vedoucí práce)
Předkládaná práce je zaměřena na popis aproximativních technik pro analýzu Markovských řetězců, konkrétně na metody založené na agregaci nebo ořezávání stavového prostoru. Na začátku je představen postup umožňující aplikaci agregace pro modely diskrétního času s libovolnou strukturou stavového prostoru a je odvozen lepší odhad aproximační chyby. Daný postup je pak propojen s uniformizačními technikami, jak se standardní tak s adaptivní, což umožňuje provádět analýzu řetězců spojitého času spolu s odhadem aproximační chyby. Navržená technika spolu s existujícími metodami založenými na ořezávání byly implementovány v rámci nástroje PRISM. Provedené experimenty potvrzuji, že nově odvozený odhad aproximační chyby vylepšuje přesnost o několik řádů bez zhoršení celkové výkonnosti. Je ukázano, že výsledná agregační metoda je schopna poskytnout validní aproximaci modelu spolu s adekvátními odhady aproximační chyby, a to jak v diskrétním tak i ve spojitém čase. Následně je provedeno porovnání s technikami založenými na ořezávání stavového prostoru a je diskutováno pro které třídy Markovských řetězců je ta či ona metoda použitelnější. Nakonec je demonstrováno úspěšne použití aproximativních technik pro model checking Markovových modelů.
|
|
|
Syntéza pravděpodobnostních programů s optimální cenou
Hranička, Vojtěch ; Síč, Juraj (oponent) ; Češka, Milan (vedoucí práce)
Tato práce se zabývá syntézou pravděpodobnostních modelů s optimální cenou. Pravděpodobnostní syntéza slouží k automatickému návrhu systému, který splňuje požadované specifikace. V této práci se věnuji způsobu syntézy kde máme šablonu pro daný systém, která obsahuje neznámé části a cílem je najít takovou kombinaci nastavení daných částí tak, aby výsledný systém splňoval specifikované požadavky. V poslední době se objevují nové přístupy uvažující o množině řešení jako o rodině Markovových řetězců. Jedním z těchto přístupů je použití nové metody kombinující metody protipříklady řízeného zjemňování abstrakce a induktivní syntézy. Tato metoda svou efektivitou převyšuje ostatní metody pro pravděpodobnostní syntézu. V této práci se konkrétně zaměřuji na rozšíření specifikačního jazyka tohoto nástroje o možnost použití takzvaných rewardů a until vlastností. Díky těmto rozšířením je možné lépe a jednodušeji specifikovat hledané řešení. Experimenty demonstrují, že i po rozšíření daného nástroje o tyto možnosti specifikace jeho rychlost v porovnání se standardní metodou syntézy zůstává až o několik řádů efektivnější.
|
|
|
GPU-Accelerated Synthesis of Probabilistic Programs
Marcin, Vladimír ; Matyáš, Jiří (oponent) ; Češka, Milan (vedoucí práce)
This paper examines the problem of automatic synthesis of probabilistic programs: having a finite family of candidate programs, how can one efficiently identify a program that satisfies a given specification. Even the most straightforward synthesis problems prove to be NP-hard. An improvement to this state of practice is brought by the PAYNT tool, which tackles this problem with a novel integrated technique for synthesising probabilistic programs. Even though it efficiently deals with the exponential growth of the family size, there is still a problem with the underlying state-space explosion. To solve this problem, we have implemented GPU-oriented model-checking algorithms that takes advantage of the GPU architecture and parallelise the task at a state level of a probabilistic model. The overall acceleration that we were able to achieve with this approach was, under certain conditions, close to the theoretically possible limit of the acceleration of the whole synthesis process.
|
|
|
Beat Grep with Counters, Challenge
Horký, Michal ; Češka, Milan (oponent) ; Holík, Lukáš (vedoucí práce)
Regular expression matching has an irreplaceable role in software development. The speed of the matching is crucial since it can have a significant impact on the overall usability of the software. However, standard approaches for regular expression matching suffer from high complexity computation for some kinds of regexes. This makes them vulnerable to attacks based on high complexity evaluation of regexes (so-called ReDoS attacks). Regexes with counting operators, which often occurs in practice, are one of such kind. Succinct representation and fast matching of such regexes can be archived by using a novel counting-set automaton. We present a C++ implementation of a matching algorithm based on the counting-set automaton. The implementation is done within the RE2 library, which is a fast state-of-the-art regular expression matcher. We perform experiments on real-life regexes. The experiments show that implementation within the RE2 is faster than the original C# implementation.
|
|
|
Rozšíření nástroje ANaConDa pro dynamickou analýzu paralelních programů
Horňák, Michal ; Češka, Milan (oponent) ; Vojnar, Tomáš (vedoucí práce)
Cieľom tejto práce bolo implementácia algoritmu FastTrack pre dynamickú analízu viacvláknových programov v jazyku C/C++. Ide o algoritmus detekujúci chyby typu data race. Je založený na relácii happens-before zakódovanej do tzv. vektor-klokov. Tie umožňujú extrapolovať beh programu a odhaľovať tak potenciálne chyby, ktoré sa v aktuálnom behu nevyskytli, ale v iných exekúciách by sa mohli vyskytnúť. Algoritmus je implementovaný v prostredí ANaConDA. Jedná sa o nástroj slúžiaci pre jednoduchšie implementovanie dynamických analizátorov monitorujúcich paralelné program na binárnej úrovni. ANaConDA poskytuje analyzátorom potrebné informácie o behu programu, ktoré detektory následne využívajú k odhaľovaniu chýb.
|
|
|
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.
|
|
|
Nástroj pro tvorbu CEG grafů
Mutňanský, Filip ; Češka, Milan (oponent) ; Smrčka, Aleš (vedoucí práce)
Testovanie pomocou grafov príčin a dôsledkov je jeden z prístupov ku testovaniu na základe požiadaviek. Grafy príčin a dôsledkov (angl. Cause-Effect Graph, CEG) sa používajú na vizualizáciu logických vzťahov medzi požiadavkami a na vyplnenie rozhodovacej tabuľky na vytvorenie testovacích prípadov. Cieľom tejto bakalárskej práce je navrhnúť a implementovať nástroj na vytváranie a manipuláciu s grafmi príčin a dôsledkov. Vytvorený nástroj je implementovaný ako single-page webová apikácia. Manipulácia s grafom je možná cez grafické rozhranie, alebo cez textovú definíciu grafu v jazyku vytvorenom pre CEG. Nástroj používa logic solver na uľahčenie vytvárania rozhodovacej tabuľky užívateľovi.
|
|
|
An Automata-Based Decision Procedure
Hečko, Michal ; Češka, Milan (oponent) ; Lengál, Ondřej (vedoucí práce)
Presburger arithmetics (PrA) is a decidable, first-order theory of natural numbers, with applications in many areas in formal verification of software properties. SMT-solvers tools implementing various algorithmic approaches to deciding whether a formula has a solution play a crucial role in formal verification. In this work, we document building a novel automatic SMT solver for PrA based on finite automata an approach that no SMT solver currently employs. We provide an overview of challenges and their solutions arising from the complexity of such a tool, including results from the conducted experiments already showing problems in which this alternative approach outperforms the state-of-the-art solvers. We have also identified problems in which the performance of the automata-based procedure struggles, which are open research opportunities.
|
|
|
Vizualizace práce CPU
Ďurčo, Marián ; Češka, Milan (oponent) ; Vojnar, Tomáš (vedoucí práce)
Táto práca má slúžiť, ako doplnok výučby na tému RISC pipeline. Samotná práca je tvorená, ako webová aplikácia. Po preskúmaní rôznych nástrojov a knižníc vhodných na túto prácu sme zvolili hlavné dve knižnice React a Redux. Vytvorené riešenie umožňuje podľa vstupu inštrukcií zobraziť inštrukčný tok v RISC pipeline a zároveň stavy registrov a pamäte. Umožňuje jednoduchým spôsobom vykonávanie prechodov medzi jednotlivými časťami vizualizácie. Na základe danej vizualizácie je možné základné pochopenie princípov RISC pipeline a jednotlivých inštrukcií asembleru.
|
host ::
RSS.