|
|
Analysis and Testing of Concurrent Programs
Letko, Zdeněk ; Lourenco, Joao (oponent) ; Sekanina, Lukáš (oponent) ; Vojnar, Tomáš (vedoucí práce)
The thesis starts by providing a taxonomy of concurrency-related errors and an overview of their dynamic detection. Then, concurrency coverage metrics which measure how well the synchronisation and concurrency-related behaviour of tested programs has been examined are proposed together with a~methodology for deriving such metrics. The proposed metrics are especially suitable for saturation-based and search-based testing. Next, a novel coverage-based noise injection techniques that maximise the number of interleavings witnessed during testing are proposed. A comparison of various existing noise injection heuristics and the newly proposed heuristics on a set of benchmarks is provided, showing that the proposed techniques win over the existing ones in some cases. Finally, a novel use of stochastic optimisation algorithms in the area of concurrency testing is proposed in the form of their application for finding suitable combinations of values of the many parameters of tests and the noise injection techniques. The approach has been implemented in a prototype way and tested on a set of benchmark programs, showing its potential to significantly improve the testing process.
|
|
|
Relational Verification of Programs with Integer Data
Konečný, Filip ; Bouajjani, Ahmed (oponent) ; Jančar, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
This work presents novel methods for verification of reachability and termination properties of programs that manipulate unbounded integer data. Most of these methods are based on acceleration techniques which compute transitive closures of program loops. We first present an algorithm that accelerates several classes of integer relations and show that the new method performs up to four orders of magnitude better than the previous ones. On the theoretical side, our framework provides a common solution to the acceleration problem by proving that the considered classes of relations are periodic. Subsequently, we introduce a semi-algorithmic reachability analysis technique that tracks relations between variables of integer programs and applies the proposed acceleration algorithm to compute summaries of procedures in a modular way. Next, we present an alternative approach to reachability analysis that integrates predicate abstraction with our acceleration techniques to increase the likelihood of convergence of the algorithm. We evaluate these algorithms and show that they can handle a number of complex integer programs where previous approaches failed. Finally, we study the termination problem for several classes of program loops and show that it is decidable. Moreover, for some of these classes, we design a polynomial time algorithm that computes the exact set of program configurations from which nonterminating runs exist. We further integrate this algorithm into a semi-algorithmic method that analyzes termination of integer programs, and show that the resulting technique can verify termination properties of several non-trivial integer programs.
|
|
|
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.
|
|
|
Simulace a protiřetězce pro efektivní práci s konečnými automaty
Holík, Lukáš ; Černá, Ivana (oponent) ; Jančar, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis is focused on techniques for finite automata and their use in practice, with the main emphasis on nondeterministic tree automata. This concerns namely techniques for size reduction and language inclusion testing, which are two problems that are crucial for many applications of tree automata. For size reduction of tree automata, we adapt the simulation quotient technique that is well established for finite word automata. We give efficient algorithms for computing tree automata simulations and we also introduce a new type of relation that arises from a combination of tree automata downward and upward simulation and that is very well suited for quotienting. The combination principle is relevant also for word automata. We then generalise the so called antichain universality and language inclusion checking technique developed originally for finite word automata for tree automata. Subsequently, we improve the antichain technique for both word and tree automata by combining it with the simulation-based inclusion checking techniques, significantly improving efficiency of the antichain method. We then show how the developed reduction and inclusion checking methods improve the method of abstract regular tree model checking, the method that was the original motivation for starting the work on tree automata. Both the reduction and the language inclusion methods are based on relatively simple and general principles that can be further extended for other types of automata and related formalisms. An example is our adaptation of the reduction methods for alternating Büchi automata, which results in an efficient alternating automata size reduction technique.
|
|
|
Analýza a oznámení o nových ResultCloud výsledcích
Iakymets, Bohdan ; Vojnar, Tomáš (oponent) ; Šimková, Hana (vedoucí práce)
Většinou výsledky testů aplikace jsou stejné a proto nenesou žádnou užitečnou informaci. Vývojáři musejí neustále probírat velké množství zbytečných informací, aby našli něco za jímavého. Tedy vývojář potřebuje nástroj pro analýzu testovacích výsledků a v případě nalezení zajimavé informace to oznámí uživateli. Tento nástroj ušetří spoustu času. Zadání této bakalářské práce je navrhnout a implementovat, mechanismus pro analýzu a oznámení uživateli o zajímavých změnách v výsledcích sady testů. Mechanismy musejí být snadno rozšiřitelné a dobře integrovatelné v ResultCloud. Součástí této práce je prostu dování ResultCloud a na základě získaných znalostí rozšíření ResultCloud o analyzátor a oznamovatele. Nástroj je implementován pomocí AngularJS a PHP.
|
|
|
A Converter between the LESS and SASS Stylesheet Formats
Večerek, Attila ; Janků, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
The aim of this thesis is to research the differences between the CSS preprocessor languages, namely Less and Sass, and find applicable transformation methods to implement a converter between their dynamic stylesheet formats. A general introduction to the concept of CSS preprocessors is provided first, which is followed by a thorough description of the Less and Sass language features. In addition to this, all the discovered differences are stated and illustrative examples of the invented conversion methods are provided in this work. This is followed by the description of the design and implementation of the proposed converter. As a part of the contribution of this thesis, a CSS comparison tool based on abstract syntax tree transformation has also been developed. Its design is described along the testing procedure used to verify the invented conversion methods. The last part of the work summarizes the achieved results and the future directions of the converter.
|
|
|
Improved Tools for Handling deltarpm Files
Chalk, Matěj ; Hruška, Martin (oponent) ; Vojnar, Tomáš (vedoucí práce)
RPM packages are used for software installation in Fedora. Every version of software packaged in this way corresponds to a separate RPM file. Updating software therefore entails downloading a large RPM file that is actually quite similar to the RPM already installed. An alternative for software updates is provided by DeltaRPM packages, which are special patch files that store the difference between two RPM files. An update then consists of downloading a much smaller file and applying this patch to the older version of the RPM. The deltarpm project defines the format of DeltaRPM files and supplies command-line tools for creating and applying them. However, this implementation is unsuitable for use as a library. The aim of this thesis is to create a new implementation of these tools, which is backwards compatible and provides a library for C developers that solves some of the weaknesses of the current implementation.
|
|
|
Editor dialogů v AngularJS pro ManageIQ
Blanco, Roman ; Pluháčková, Hana (oponent) ; Vojnar, Tomáš (vedoucí práce)
Hlavním cílem této bakalárské práce je návrh a implementace řešení pro editor dialogů pro aplikaci ManageIQ. Nový editor by měl být vytvořený jako jedno-stránová aplikace vytvořená pomocí JavaScriptové knihovny AngularJS a drag&drop techniky. Řešení mělo poskytnout komfortnější rozhraní koncovým uživatelůn, než nabízí současná implementace.
|
|
|
SELinux Policy Analysis Tool
Mojžíš, Vít ; Peringer, Petr (oponent) ; Vojnar, Tomáš (vedoucí práce)
This thesis deals with mandatory access control (MAC)-based security module policy analysis, focusing on SELinux. Because of insuffient capabilities of available analysis tools, new tool was designed and implemented with the needs of Red Hat SELinux team in mind. Its main uses will be as aid in policy development and support in SELinux usefulness evaluation. If the tool proves useful, it will be incorporated into SELinux userspace tools package SETools 4.
|
|
|
Předpověď nových chyb pomocí dolování dat v historii výsledků testů
Matys, Filip ; Vojnar, Tomáš (oponent) ; Šimková, Hana (vedoucí práce)
Softwarové projekty prochází jak obdobím údržby, tak v případě open source i náročným neřízeným vývojem. Obě tyto fáze jsou náchylné k regresím, tedy chybám vedoucím k degradaci již fungujících částí systému. Z tohoto důvodu je systém podrobován testováním v podobě testovacích sad, což je v mnoha případech časově velmi náročné. Z tohoto důvodu vznikají prediktory, které jsou schopny na základě změn kódu a historie testování odhadnout, kdy k takovým regresím může dojít, pomocí čehož pak lze testování soustředit na tato místa. Tyto prediktory jsou však často postaveny na metrikách kódu, které jsou čistě statické a neřeší sémantiku daného jazyka. Účelem této diplomové práce je vytvořit prediktor, který nebude spoléhat jen na tyto metriky, ale bude schopen analyzovat kód i ze sémantického pohledu.
|
host ::
RSS.