|
|
Synthesizing Non-Termination Proofs from Templates
Martiček, Štefan ; Fiedor, Tomáš (referee) ; Vojnar, Tomáš (advisor)
Jednou z nejsložitěji verifikovaných vlastností programů v oblasti formální analýzy je živost. K jedné z metod ověřujících tuto vlastnost patří i dokazování neukončitelnosti programů. Naše práce popisuje návrh a implementaci dvou algoritmů ověřujících neukončitelnost. Inspirujeme se již existujícími přístupy, jako jsou rekurentní množiny a nadaproximace cyklů s využitím invariantů ve tvaru rekurentních relací. Hlavní výzvu pro nás představovalo přizpůsobení těchto algoritmů SSA (single static assignment) reprezentaci použité v 2LS a jejich celková integrace v našem frameworku. Vzpomínané přístupy se nám podařilo spojit do analýzy neukončitelnosti, která dosahuje nejlepší výsledky v porovnání s existujícími nástroji, které byly srovnané na soutěži SV-COMP 2017.
|
|
|
Selected Extensions of the Albegraic System Octave
Salač, Radek ; Smrčka, Aleš (referee) ; Vojnar, Tomáš (advisor)
This work deals with issues linked to solving system of linear equations in the environment of numerical computer. It describes the fundamental algorithms emphasizing their positive as well as negative sides. The work is devoted to general issues such as time complexity and memory demandingness of given algorithms. In the last part, the process of implementation of selected procedures into the algebraic system Octave is described.
|
|
|
Plugins for Getting Information about the System for BusyBox
Poláček, Marek ; Konečný, Filip (referee) ; Vojnar, Tomáš (advisor)
In this thesis, we discuss implementation of tools for getting information from the system. We examine file systems sysfs and procfs in the Linux operating system. Furthermore, we discourse how to write small programs in the C language. Eventually, we take a look at implementation of tools like iostat, mpstat and powertop. These tools were implemented in a minimalistic form suitable for Busybox within this thesis.
|
|
|
A GUI for Configuring an FTP Server
Barabas, Maroš ; Janoušek, Vladimír (referee) ; Vojnar, Tomáš (advisor)
The subject of this document is concept and implementation of graphical configuration tool for vsftpd ftp server, which is distributed to Red Hat Linux operating systems. Mainly, the document puts accent on simplicity of user's access to server configuration, complexity of access to configuration options and their scalability. The program is integrated to GNOME desktop enviroment.
|
|
|
Automatic Component Metadata Extractor and Consolidator for Continuous Integration
Kulda, Jiří ; Smrčka, Aleš (referee) ; Vojnar, Tomáš (advisor)
Tato diplomová práce popisuje úpravu průběžné integrace pro Platform tým ve společnosti Red Hat. Výsledkem práce je nástroj Metamorph, který umožní sjednocení ostatních nástrojů průběžné integrace pod týmem Platform. Teoretická část popisuje vznik, popis a přidané hodnoty průběžné integrace. Následně jsou blíže přiblíženy existující nástroje na trhu. Dále je zde popsáno použití průběžné integrace v nástroji Jenkins. V práci jsou také dopodrobna popsány existující řešení průběžné integrace ve společnosti Red Hat. Dále je zde popsán návrh a implementace výše zmíněného nástroje. V závěru jsou výsledky práce otestovány týmem z firmy Red Hat a nastíněny možnosti rozšíření.
|
|
|
Dynamic Data Race Detection and Self-Healing in Java Programs
Letko, Zdeněk ; Kolář, Dušan (referee) ; Vojnar, Tomáš (advisor)
Finding concurrency bugs in complex software is difficult. As a contribution to coping with this problem the thesis proposes an architecture for a fully automated dynamic detection and healing of data races and atomicity violations in Java. Two distinct algorithms for detecting of data races are presented. One of them is a novel algorithm called AtomRace which detects data races as a special case of atomicity violations. The healing is based on suppressing a recurrence of the detected problem and can be performed by introducing an additional synchronization or by legally influencing the Java scheduler. Basically forces certain parts of the code to be executed atomically. The proposed architecture uses bytecode instrumentation to be able to track and influence the execution. The architecture and algorithms were implemented and tested on multiple case studies.
|
|
|
Application of Genetic Algorithms and Data Mining in Noise-based Testing of Concurrent Software
Šimková, Hana ; Kofroň, Jan (referee) ; Lourenco, Joao (referee) ; Vojnar, Tomáš (advisor)
Tato práce navrhuje zlepšení výkonu testování programů použitím technik dolování z dat a genetických algoritmů při testování paralelních programů. Paralelní programování se v posledních letech stává velmi populárním i přesto, že toto programování je mnohem náročnějsí než jednodušší sekvenční a proto jeho zvýšené používání vede k podstatně vyššímu počtu chyb. Tyto chyby se vyskytují v důsledku chyb v synchronizaci jednotlivých procesů programu. Nalezení takových chyb tradičním způsobem je složité a navíc opakované spouštění těchto testů ve stejném prostředí typicky vede pouze k prohledávání stejných prokládání. V práci se využívá metody vstřikování šumu, která vystresuje program tak, že se mohou objevit některá nová chování. Pro účinnost této metody je nutné zvolit vhodné heuristiky a též i hodnoty jejich parametrů, což není snadné. V práci se využívá metod dolování z dat, genetických algoritmů a jejich kombinace pro nalezení těchto heuristik a hodnot parametrů. V práci je vedle výsledků výzkumu uveden stručný přehled dalších Technik testování paralelních programů.
|
|
|
Grammars with Restricted Derivation Trees
Koutný, Jiří ; Janoušek, Jan (referee) ; Vojnar, Tomáš (referee) ; Meduna, Alexandr (advisor)
V této disertační práci jsou studovány teoretické vlastnosti gramatik s omezenými derivačními stromy. Po uvedení současného stavu poznání v této oblasti je výzkum zaměřen na tři základní typy omezení derivačních stromů. Nejprve je představeno zcela nové téma, které je založeno na omezení řezů a je zkoumána vyjadřovací síla takto omezené gramatiky. Poté je zkoumáno několik nových vlastností omezení kladeného na cestu derivačních stromů. Zejména je studován vliv vymazávacích pravidel na vyjadřovací sílu gramatik s omezenou cestou a pro tyto gramatiky jsou zavedeny dvě normální formy. Následně je popsána nová souvislost mezi gramatikami s omezenou cestou a některými pseudouzly. Dále je prezentován protiargument k vyjadřovací síle tohoto modelu, která byla dosud považována za dobře známou vlastnost. Nakonec je zavedeno zobecnění modelu s omezenou cestou na ne jednu, ale několik cest. Tento model je následně studován zejména z hlediska vlastností vkládání, uzávěrových vlastností a vlastností syntaktické analýzy.
|
|
|
Firefox OS Application for Learning Languages
Chudík, Jakub ; Fiedor, Tomáš (referee) ; Vojnar, Tomáš (advisor)
Tato práce se zabývá vytvořením aplikace pro výuku jazyků specificky pro mobilní operační systém Firefox OS. Vzhledem k své povaze, uživatelské rozhraní aplikace se snaží uspokojit ergonomické potřeby aplikací určených pro kapesní zařízení. Aplikuje několik konceptů gamifikace ke zlepšení procesu učení, jehož výsledky jsou prezentovány a vyhodnoceny. Aplikace také přináší své vlastní jedinečné vlastnosti, které jí pomáhají vyniknout mezi ostatními aplikacemi pro výuku jazyků.
|
|
|
Automated Test Documentation Generator for BeakerLib Tests
Kulda, Jiří ; Smrčka, Aleš (referee) ; Vojnar, Tomáš (advisor)
The aim of this work in cooperation with Red Hat Czech company is to design, implement and verify documentation generator for test written using BeakerLib library, which effectively creates documentation from BeakerLib tests without any documentation markup. In the first step generator parses data from every BeakerLib command in the test. Subsequently data are transformed as a natural language information. At the end generator transforms this information into documentation template. In this case an argparse method was used to find possible data from BeakerLib commands. In contrast to existing documentation generators this generator brings a new way of documentary creation from tests without any documentation markup. Thanks to this point of view we can generate documentation, which is created on base of automated understanding of test source code. Through documentation generator development time the generator was tested on three BeakerLib tests. In the end the documentation generator was tested on ten BeakerLib tests which were randomly selected.
|
guest ::
