|
| |
|
|
Next Generation of Rank-Based Algorithms for Omega Automata
Šmahlíková, Barbora ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
Büchi automata (BA) complementation is a crucial operation for termination analysis of programs, model checking, or decision procedures for various logics. Despite its prominence, practically efficient algorithms for BA complementation are still missing. This thesis deals with optimizations of Büchi automata complementation, focusing mainly on rank-based techniques. The original rank-based algorithm is asymptotically optimal, but it can still generate unnecessarily large state space. For a practical usage, it is therefore desirable to reduce the number of generated states in the complement as much as possible. We propose several techniques that can efficiently complement some special types of Büchi automata, occuring often in practice, based on their structure. Some of these techniques can also, to a certain degree, be extended to general Büchi automata. The developed techniques were implemented as an extension of the tool Ranker for Büchi automata complementation and evaluated on thousands of hard automata. Our optimizations significantly reduce the generated state space and Ranker produces in the majority of cases a~smaller complement than other state-of-the-art tools.
|
|
|
Generic Template-Based Synthesis of Program Abstractions
Marušák, Matej ; Holík, Lukáš (oponent) ; Malík, Viktor (vedoucí práce)
The goal of this work is to design and to implement a generic strategy solver to the 2LS tool. 2LS is an analyser for a static verification of programs written in C language. A verified program is analysed by an SMT solver using abstract interpretation. Convertion from an abstract state of the program into a logical formula, that an SMT solver can work with, is done by a component called strategy solver. In the current implementation, there is one strategy solver for each abstract domain. Our approach introduces a single generic strategy solver, which makes creating new domains easier. Also, this approach enables migration of the existing domains and hence the codebase can be reduced.
|
|
|
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.
|
|
|
Generování strukturovaných testovacích dat
Olšák, Ondřej ; Holík, Lukáš (oponent) ; Smrčka, Aleš (vedoucí práce)
Cílem této práce je vytvořit nástroj umožňující generovat soubory obsahující strukturovaná data za účelem testování na základě vstupních domén. Tato práce se soustředí na stromově strukturovaná data. Nástroj integruje již dříve implementované nástroje pro tvorbu testovacích dat splňujících uživatelem vybrané kritérium pokrytí vstupních domén. Vytvořený nástroj je schopen generovat sady testovacích souborů ve formátu JSON a XML s testovacími daty, které splňují kritérium pokrytí ECC, BCC nebo PWC.
|
|
|
A Library for Binary Decision Diagrams
Paulovčák, Martin ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
The aim of this thesis is to create an easy-to-use library that will provide the basic means for Boolean function manipulation based on six different variants of Binary Decision Diagrams - BDD, ZDD, CBDD, CZDD, TBDD, and ESRBDD. The library is implemented in the ISO C programming language, uses closed hashing, index-based node referencing, mark and sweep based garbage collector and diagram construction is based on classical depth-first traversal. The implemented variants of these diagrams were compared on benchmarks and although the optimal choice of decision diagram variant depends on given problem, in general TBDD proved to be the best choice in terms of the resulting graph size and also CPU time.
|
|
|
Pokrytelnosti pro paralelní programy
Turoňová, Lenka ; Vojnar, Tomáš (oponent) ; Holík, Lukáš (vedoucí práce)
Tato diplomová práce se zabývá automatickou verifikací systémů s paralelně běžícími procesy. Práce diskutuje existující metody a možnosti jejich optimalizace. Stávající techniky jsou založeny na hledání induktivního invariantu (například pomocí techniky zjemňování abstrakce řízené protipříklady (CEGAR)). Efektivnost metod závisí na velikosti nalezeného invariantu. V rámci této diplomové práce jsme nalezli možnost zlepšení metod díky zaměření se na hledání invariantů minimální velikosti. Naimplementovali jsme nástroj, který zajišťuje prohledávání prostoru invariantů systému. Naše experimentální výsledky ukazují, že mnoho existujících systémů užívaných v praxi má skutečně mnohem menší invarianty než ty, které lze nalézt stávajícími metodami. Závěry a výsledky této práce budou sloužit jako základ budoucího výzkumu, jehož cílem bude navržení optimální metody pro vypočítání malých invariantů paralelních systémů.
|
|
|
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.
|
|
|
Verifikovaná knihovna datových struktur
Rychnovský, Jan ; Holík, Lukáš (oponent) ; Lengál, Ondřej (vedoucí práce)
Tato bakalářská práce se zabývá metodikou psaní verifikovaných programů pomocí nástroje VCC. Zmíněná metodika je založena na principu doplnění kódu programu o anotace, jež poskytují specifikaci požadované funkcionality. Nástroj VCC pak prostřednictvím formálních metod určí zda zdrojový kód splňuje danou specifikaci či ne. V první části práce je popsána formální verifikace a zmíněny tři základní přístupy k ní. Následně jsou popsány problémy splnitelnosti výrokových formulí (SAT) a splnitelnosti formulí v teoriích predikátové logiky (SMT). Práce se dále věnuje popisu verifikačního nástroje VCC, jeho funkčnosti, metodice, syntaxi a sémantice příkazů jeho anotačního jazyka BoogiePL. Druhá část textu je zaměřena na popis návrhu a implementace verifikované knihovny datových struktur obsahující jednosměrný, dvousměrný a kruhový seznam, binární vyhledávací strom a Treiberův zásobník. Závěr práce diskutuje získané poznatky o programovací metodice založené na psaní verifikovaného kódu.
|
|
|
Testování platformy JBoss Drools založené na modelu
Široký, Petr ; Holík, Lukáš (oponent) ; Letko, Zdeněk (vedoucí práce)
Technika testování založeného na modelu (MBT) využívá model chování systému k automatickému generování sady testů, čímž snižuje nákladnost testování oproti konvenčnímu manuálnímu vývoji a udržbě testů. Tato práce se zaměřuje na využití zvoleného MBT nástroje OSMO při testování reálného softwarového produktu. Konkrétně se o jedná kompilátor podnikových pravidel využívaný v systému Drools, který je spoluvyvíjený společností Red Hat. V práci je popsán způsob zavedení MBT přístupu s ohledem na jeho dobré přijetí komunitou vývojářů, dále pak vytvoření modelu možných vstupů testovaného kompilátoru a zhodnocení vytvořené testovací sady. Využití MBT přístupu vedlo k odhalení pěti nahlášených a tří potencionálních a dosud nehlášených chyb v testovaném kódu. Práce na příkladu shrnuje hlavní přednosti i praktické nedostatky využití MBT technik v praxi.
|
host ::
RSS.