|
|
Synthesizing Non-Termination Proofs from Templates
Martiček, Štefan ; Fiedor, Tomáš (oponent) ; Vojnar, Tomáš (vedoucí práce)
One of the properties that are most difficult to verify in the area of formal analysis is liveness. Proving non-termination of programs also belongs to the methods that verify this property. Our work describes the design and implementation of two algorithms checking non-termination. We inspire ourselves by already existing approaches, such as recurrence sets and over-approximation of loops with the use of invariants in the form of recurrence relations. The main challenge for us was an adaptation of these algorithms to the SSA (single static assignment) representation used in 2LS and the overall integration in our framework. We were able to unify the mentioned approaches into analysis of non-termination, which achieves the best results in comparison to the other tools that were compared at the SV-COMP 2017 competition.
|
|
|
Vybraná rozšíření algebraického systému Octave
Salač, Radek ; Smrčka, Aleš (oponent) ; Vojnar, Tomáš (vedoucí práce)
Práce se zabývá problematikou řešení soustavy lineárních rovnic v prostředí číslicového počítače. Popisuje základní používané algoritmy s důrazem na jejich silné a slabé stránky. Věnuje se obecným problémům jako je časová složitost a paměťová náročnost daných algoritmů. V závěru popisujeme průběh implementace vybraných procedur do algebraického systému Octave.
|
|
|
Pluginy pro získávání informací o systému pro projekt BusyBox
Poláček, Marek ; Konečný, Filip (oponent) ; Vojnar, Tomáš (vedoucí práce)
Tato práce se zabývá implementací nástrojů pro získávání informací o operačním systému pro projekt Busybox. Diskutovány jsou souborové systémy sysfs a procfs v operačním systému Linux. Dále se práce zabývá tím, jak vytvářet co nejmenší programy v jazyce C. Také se věnuje struktuře programů iostat, mpstat a powertop. V rámci práce byly vytvořeny minimalistické implementace již existujících nástrojů, zejména z balíku sysstat, který obsahuje například utility iostat a mpstat.
|
|
|
GUI pro konfiguraci FTP serveru
Barabas, Maroš ; Janoušek, Vladimír (oponent) ; Vojnar, Tomáš (vedoucí práce)
Obsahom tejto bakalárskej práce je návrh a implementácia grafického konfiguračného nástroja pre ftp server vsftpd, distribuovaný do operačných systémov Red Hat Linux. Dôraz je kladený na jednoduchosť prístupu užívateľov ku konfigurácii servera, komplexnosť v prístupe ku konfiguračným možnostiam a ich škálovateľnosť. Program je integrovaný do desktopového prostredia GNOME.
|
|
|
Automatic Component Metadata Extractor and Consolidator for Continuous Integration
Kulda, Jiří ; Smrčka, Aleš (oponent) ; Vojnar, Tomáš (vedoucí práce)
This Master Thesis focuses on the modification of continuous integration practice within the Platform team at Red Hat. The result of this thesis is the Metamorph, tool which will make it possible to unify the continuous integration tools of sub teams under the Platform team. The theoretical part describes the creation of a continuous integration practice and explains its benefits. Subsequently, existing CI tools (in the industry) are presented in detail. The following section demonstrates how continuous integration uses the Jenkins tool. This master thesis also contains the particulars of existing internal CI solutions at Red Hat. In the practical part, the design and implementation of tool that was made during the creation of this master thesis are introduced. In conclusion, the results are tested by one team at Red Hat and a possible extension is outlined.
|
|
|
Dynamická detekce a léčení časově závislých chyb nad daty v prostředí Java
Letko, Zdeněk ; Kolář, Dušan (oponent) ; Vojnar, Tomáš (vedoucí práce)
Hledání chyb plynoucích ze souběžného zpracovávání výpočtů je obtížné. Proto se tato diplomová práce zabývá detekcí a léčením časově závislých chyb nad daty a chyb plynoucích z nesprávné atomicity operací v prostředí Java. Práce prezentuje dva různé algoritmy pro detekci. Jedním z nich je nový algoritmus nazvaný AtomRace, který detekuje časově závislé chyby nad daty jako speciální případ nesprávné atomicity operací. Následné léčení detekovaných chyb je založeno na potlačení opakování chyby, buď zavedením přídavné synchronizace, nebo legálním ovlivňováním plánovače Javy, za účelem vynucení správné atomicity operací. Navržená architektura, která pracuje souběžně se sledovaným programem, využívá ke sledování a ovlivňování výpočtu techniku instrumentace na úrovni Java bytecode. Architektura a algoritmy byly implementovány a otestovány v několika případových studiích.
|
|
|
Application of Genetic Algorithms and Data Mining in Noise-based Testing of Concurrent Software
Šimková, Hana ; Kofroň, Jan (oponent) ; Lourenco, Joao (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis proposes an improvement of the efficiency of testing concurrent software by employing data mining techniques and genetic algorithms in the process of testing concurrent software. Concurrent, or multi-threaded, programming has become very popular over the last few years. However, as the concurrent programming is far more demanding the sequential programming, its increased use leads to a significant increase in the number of errors that appear in commercial software due to errors in synchronization. Finding such errors using traditional testing methods is difficult. Moreover, repeated test executions of traditional testing that are performed in the same environment will typically examine similar interleavings only. Hence, the noise-based injection approach is used for influencing the scheduling by injecting various kinds of noise (delays, context switches, and so on) into the common thread behaviour which stress the software and can to show some rare behaviour. However, for the noise injection to be efficient, one has to choose suitable noise injection heuristics from among the many existing ones as well as to suitably choose values of their various parameters, which is not easy. In this work, there are used data mining methods and genetic algorithms and their combinations to deal with the problem of choosing such noise injection heuristics and values of their parameters. Besides setting up of the goals of the thesis, this proposal also provides a brief summary of the state of the art in application of data mining techniques and genetic algorithms to program testing problems.
|
|
|
Grammars with Restricted Derivation Trees
Koutný, Jiří ; Janoušek, Jan (oponent) ; Vojnar, Tomáš (oponent) ; Meduna, Alexandr (vedoucí práce)
This doctoral thesis studies theoretical properties of grammars with restricted derivation trees. After presenting the state of the art concerning this investigation area, the research is focused on the three main kinds of the restrictions placed upon the derivation trees. First, it introduces completely new investigation area represented by cut-based restriction and examines the generative power of the grammars restricted in this way. Second, it investigates several new properties of path-based restriction placed upon the derivation trees. Specifically, it studies the impact of erasing productions on the generative power of grammars with restricted path and introduces two corresponding normal forms. Then, it describes a new relation between grammars with restricted path and some pseudoknots. Next, it presents a counterargument to the generative power of grammars with controlled path that has been considered as well-known so far. Finally, it introduces a generalization of path-based restriction to not just one but several paths. The model generalized in this way is studied, namely its pumping, closure, and parsing properties.
|
|
|
Firefox OS Application for Learning Languages
Chudík, Jakub ; Fiedor, Tomáš (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis deals with creating a language learning application specifically for the Friefox OS operating system for mobile, handheld devices. Because of its nature, the application's user interface attempts to cater specifically to the ergonomic needs of applications for handheld devices. It applies several concepts of gamification to improve the language learning process, the results of which are presented and evaluated. The application also brings its own unique features to make it stand out among existing state of art language learning applications.
|
|
|
Generátor dokumentace pro testy používající knihovnu BeakerLib
Kulda, Jiří ; Smrčka, Aleš (oponent) ; Vojnar, Tomáš (vedoucí práce)
Cílem této práce řešené ve spolupráci se společností Red Hat Czech je navrhnout, implementovat a ověřit generátor dokumentace pro testy používající knihovnu BeakerLib, který efektivně vytváří dokumentaci z neokomentovaných BeakerLib testů. V prvním kroku generátor extrahuje data z BeakerLib příkazů. Následně jsou data přetvořena do informací v přirozeném jazyce. Na závěr jsou tyto informace vloženy do šablony dokumentace. Při tvorbě generátoru dokumentace byl použit modul argparse pro hledání dat z BeakerLib příkazů. Ve srovnání s existujícími nástroji navržený generátor přináší nový způsob vytváření dokumentací bez použití dokumentačních komentářů. Díky této vlastnosti lze generovat dokumentace, které jsou vytvořeny na základě automatizovaného porozumění zdrojového kódu testu. Testování, po celou dobu vývoje generátoru, probíhalo na třech zvolených BekerLib testech. Na závěr byl generátor otestován na deseti náhodně zvolených BeakerLib testech.
|
host ::
RSS.