|
|
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.
|
|
|
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.
|
|
|
Inkrementální induktivní pokrytelnost pro alternující konečné automaty
Vargovčík, Pavol ; Lengál, Ondřej (oponent) ; Holík, Lukáš (vedoucí práce)
V tejto práci navrhujeme špecializáciu algoritmu inductive incremental coverability, ktorá rieši problém prázdnosti alternujúcich konečných automatov. Experimentujeme s rôznymi návrhovými rozhodnutiami, analyzujeme ich a dokazujeme ich korektnosť. Aj keď je známe, že problém je sám o sebe PSpace-ťažký, zameriavame sa na to, aby bolo rozhodovanie prázdnosti výpočetne prijateľné v niektorých triedach automatov s praktickým využitím. Dosiahli sme niekoľko zaujímavýcch výsledkov v porovnaní so špičkovými algoritmami, predovšetkým v porovnaní s algoritmami založenými na protireťazcoch.
|
|
|
Podnikatelský záměr
Holík, Lukáš ; Smolíková,, Lenka (oponent) ; Heralecký, Tomáš (vedoucí práce)
Cílem diplomové práce je vytvořit podnikatelský plán pro pana Davida Mokrého, majitele kavárny s názvem Blue Queen v Boskovicích, který v blízké době chce rozšířit svoji podnikatelskou činnost o další podnik - Black King. Pomocí četných analýz trhu a analýz vnějšího i vnitřního okolí získám data potřebná k vytvoření projektu na vybudování úspěšné nové kavárny, která by se měla stát nejvyhledávanějším podnikem v okolí.
|
|
|
Kongruence pro stromové automaty
Žufan, Petr ; Janků, Petr (oponent) ; Holík, Lukáš (vedoucí práce)
Tento článek pojednává o testování ekvivalence stromových automatů (TA). Přináší nový algoritmus vycházející z algoritmu Bonchiho a Pouse pro slovní automaty. Tento nový algoritmus spojuje bisimulaci s determinizací za běhu. Pomocí optimalizace založené na kongruenčním uzávěru se snaží vyhýbat extrémnímu zvětšování stavového prostoru. Z tohoto hlediska je lepší než jiné metody pro tento problém.
|
|
|
Simulace pro symbolické automaty
Síč, Juraj ; Lengál, Ondřej (oponent) ; Holík, Lukáš (vedoucí práce)
Symbolické automaty sú podobné klasickým automatom s jedným veľkým rozdielom: prechody sú značené predikátmi definovanými v oddelenej teórii. Toto umožňuje použiť veľké abecedy s pouźitím oveľa menšieho miesta. V tejto práci sa zaoberáme výpočtom simulácie (binárnej relácie nad množinou stavov, ktorá aproximuje jazykovú inklúziu) pre tieto automaty. Táto relácia sa dá potom použiť pri redukovaní počtu stavov bez nutnosti determinizácie. Existuje niekoľko algoritomv pre výpočet simulácie pre Kripkeho štruktúry, ktoré boli neskôr modifikované pre označené prechodové systémy a klasické automaty. V tejto práci ukážeme ako sa dá jeden z týchto algoritmov modifikovať pre symbolické automaty použitím rozkladu domény abecedy ktorý je kompatibilný s predikátmi značiacimi prechody a použitím možností teórie abecedy.
|
|
|
Aritmetická úplnost logiky R
Holík, Lukáš ; Švejdar, Vítězslav (vedoucí práce) ; Bílková, Marta (oponent)
Cílem práce bylo s použitím novodobé notace vystavět teorii Rosserovy logiky, vysvětlit do detailu její vztah s Peanovou aritmetikou, ukázat kripkovskou sémantiku a nakonec pomocí autoreference v množném čísle zpracovat důkaz aritmetické úplnosti. V poslední kapitole se pak ukazují některé z vlastností rosserovských sentencí. Powered by TCPDF (www.tcpdf.org)
|
|
|
Towards Static Analysis of Languages with Dynamic Features
Hauzar, David ; Plášil, František (vedoucí práce) ; Sinz, Carsten (oponent) ; Holík, Lukáš (oponent)
Dynamické funkce programovacích jazyků, jako je dynamický typový systém, dynamické volání funkcí, dynamické vykonávání kódu a dynamické datové struktury, poskytují flexibilitu, která urychluje vývoj. Tyto funkce ale snižují množství informací, které jsou kontrolovány v době kompilace. To má za následek nižší výkon a větší chybovost programů. Tento problém je možné vyřešit pomocí technik statické analýzy. Dynamické funkce bohužel pro tyto techniky představují překážku a zásadně omezují jejich přesnost, spolehlivost a výkonnost. Abychom tento problém pomohli vyřešit, navrhujeme framework pro statickou analýzu, který automaticky řeší dynamické funkce, a tím umožňuje definovat přesné a spolehlivé statické analýzy podobně jako v případě, kdy program dynamické funkce neobsahuje. Aby bylo takový framework možné vytvořit, navrhujeme novou techniku heap analýzy, která modeluje asociativní pole a (prototypové) objekty. Dále navrhujeme analýzu hodnot proměnných, která zjišťuje další informace potřebné pro vypořádání se s dynamickými funkcemi. Nakonec navrhujeme techniku, která umožňuje automaticky a genericky kombinovat analýzu hodnot proměnných s heap analýzou. Powered by TCPDF (www.tcpdf.org)
|
|
|
Ultrapower construction in set theory
Holík, Lukáš ; Honzík, Radek (vedoucí práce) ; Verner, Jonathan (oponent)
Předložená práce obsahuje historii vzniku míry, její souvislost s měřitelnými kardinály a shrnutí všech základních definic a pojmů potřebných k zobecnění ultramocninové konstrukce v teorii modelů pro vlastní třídy. Součástí uvedené teorie je i důkaz základních vlastností potřebných pro aplikaci ultramocninové konstrukce na měřitelné kardinály. Využitím všech předchozích výsledků poté dokážeme Teorém Dany Scotta o souvislosti mezi existencí měřitelného kardinálu a velikostí univerza.
|
|
|
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.
|
host ::
RSS.