|
Analysis of drawing contributions from the Regional Operational Programme in the Košice Region 2007 - 2013
Hupka, Peter ; Kalábová, Markéta (vedoucí práce) ; Abrhám, Josef (oponent)
Regionální politika se stává jednou ze strategických priorit Evropské unie až s jejím postupným rozšířením. Hlavním nástrojem této politiky jsou dotace pro zaostalejší regiony. Tato práce má za cíl zhodnotit Regionální operační program v Košickém kraji v rámci programového období 2007 až 2013. Teoretickou částí autor popisuje proces formování Evropské unie, obecně charakterizuje eurofondy a specifikuje Slovenskou republiku a Košický kraj. Analytická část je věnována charakteristice samotného Regionálního operačního programu. Použitím metody porovnávání jsou hodnoceny jednotlivé prioritní osy operačního programu na základě úspěšnosti čerpání alokací. Pro objektivní zhodnocení byl porovnán i Košický kraj s ostatními kraji Slovenské republiky na úrovni prioritních os. Na základě analýzy autor zhodnotil Regionální operační program v Košickém kraji jako úspěšný s prostorem na zlepšení přizpůsobení alokací.
|
|
Profil a reflexe tanečního oddělení Julliard school
Červinka, Marek ; JANEČEK, Václav (vedoucí práce) ; KŘENKOVÁ, Mahulena (oponent)
Tato bakalářská práce s názvem Profil a reflexe tanečního oddělení Juilliard School se nejprve stručně věnuje klíčovým událostem v dějinách klasického i moderního tance první poloviny 20. století a dále historii The Bennington School of the Dance, která je považována za předchůdce The Juilliard School. Po všeobecných informacích ohledně historie, vzdělávacích cílů a studijních programů The Juilliard School se zbytek práce detailně zaměřuje na její Taneční fakultu. Popisuje její historii, světoznámé pedagogy, studijní program a přijímací řízení. Všechny tyto informace společně s rozhovory, které poskytl český choreograf a pedagog Jarek Cemerek a současný student čtvrtého ročníku Brennan Clost, se staly podklady pro závěrečnou reflexi této fakulty. Ta obsahuje srovnání The Juilliard School s českým tanečním školstvím.
|
|
Neinvazivní metody pro stanovení pohlaví a stereoidních hormonů u gibonů rodu Nomascus
Bolechová, Petra ; Bartoš, Luděk (vedoucí práce) ; Pavel, Pavel (oponent)
Giboni rodu Nomascus patří ke kriticky ohroženému druhu, o kterém zároveň chybí velké množství základních biologických informací. Vzhledem ke statutu těchto zvířat ve volné přírodě i počtu chovaných jedinců v chovu zoologických zahrad je prioritní otázkou zlepšení managmentu chovu, kam patří i znalost reprodukce. Základním cílem této práce je praktické využití neinvazivních metod (polymerázová řetězová reakce k extrakci DNA a enzymové imunotesty), využívajících k analýzám vzorky výkalů. První metoda, polymerázová řetězová reakce, byla využita pro determinaci pohlaví u mláďat, protože kvůli jejich specifickému zbarvení a vzhledové podobnosti vnějších pohlavních orgánů, není diagnostika možná bez odchycení zvířete. Další částí je zodpovězení hypotéz týkajících se ovariálního cyklu samic a faktorů ovlivňujících jejich koncentrace včetně souvislosti nástupu pohlavního cyklu u samic a jejich změny barvy srsti. Hypotézy byly ověřeny sledováním výše koncentrací metabolitů progesteronu a estrogenu ve výkalech a vyhodnocením složení chovné skupiny gibonů a vlivu ZOO. Celkem bylo analyzováno během čtyř let (2010-2014) 51 zvířat z 16 zoologických zahrad v celkovém množství 1618 vzorků výkalů. Výsledky potvrdily využití neinvazivních metod pro determinaci pohlaví a tak zajištění maximálního welfare v chovech. Endokrinologické analýzy potvrdily hypotézy o vlivu prostředí (ZOO) na koncentraci hormonů a vliv březosti samice a jejího věku na výši koncentrace hormonů, ale také vliv březosti na koncentraci hormonů u samců-otců. Prvotní informací v této studii je potvrzení nástupu ovariálního cyklu u mladých samic bez návaznosti na jejich přebarvení a významný faktor vlivu matky a její teritoriality. Tato studie předkládá první dlouhodobější monitoring ovariálního cyklu u samic a koncentrace hormonů u ostatních jedinců ve všech věkových kategoriích i pohlaví. Výsledky umožňují pochopit vliv chovatelského prostředí na reprodukční postavení těchto gibonů a přispívají k celkovému zlepšení managementu chovu.
|
|
Portace knihovny Prawn z Ruby do Pythonu 3
Molhanec, Michal ; Pícka, Marek (vedoucí práce) ; Mikoláš, Mikoláš (oponent)
Práce se zabývá automatickým překladem kódu napsaného v jazyku Ruby do Pythonu 3. Nejprve jsou prozkoumány principy překladu, jak je popisuje odborná literatura. V další části se porovnávají jednotlivé jazykové konstrukce a jsou navrženy způsoby jejich překladu.
Na základě této teorie byl vyvinut překladač, který svou funkčnost ukazuje na překladu knihovny Prawn pro generování PDF souborů.
|
|
Automata in Infinite-state Formal Verification
Lengál, Ondřej ; Jančar, Petr (oponent) ; Veith, Helmut (oponent) ; Esparza, Javier (oponent) ; Vojnar, Tomáš (vedoucí práce)
The work presented in this thesis focuses on finite state automata over finite words and finite trees, and the use of such automata in formal verification of infinite-state systems. First, we focus on extensions of a previously introduced framework for verifi cation of heap-manipulating programs-in particular programs with complex dynamic data structures-based on tree automata. We propose several extensions to the framework, such as making it fully automated or extending it to consider ordering over data values. Further, we also propose novel decision procedures for two logics that are often used in formal verification: separation logic and weak monadic second order logic of one successor. These decision procedures are based on a translation of the problem into the domain of automata and subsequent manipulation in the target domain. Finally, we have also developed new approaches for efficient manipulation with tree automata, mainly for testing language inclusion and for handling automata with large alphabets, and implemented them in a library for general use. The developed algorithms are used as the key technology to make the above mentioned techniques feasible in practice.
|
|
Retargetable Analysis of Machine Code
Křoustek, Jakub ; Janoušek, Jan (oponent) ; Návrat,, Pavol (oponent) ; Kolář, Dušan (vedoucí práce)
Program analysis is a computer-science methodology whose task is to analyse the behavior of a given program. The methods of program analysis can also be used in other methodologies such as reverse engineering, re-engineering, code migration, etc. In this thesis, we focus on program analysis of a machine-code and we address the limitations of a nowadays approaches by proposing novel methods of a fast and accurate retargetable analysis (i.e. they are designed to be independent of a particular target platform). We focus on two types of analysis - dynamic analysis (i.e. run-time analysis) and static analysis (i.e. analysing application without its execution). The contribution of this thesis within the dynamic analysis lays in the extension and enhancement of existing methods and their implementation as a retargetable debugger and two types of a retargetable translated simulator. Within the static analysis, we present a concept and implementation of a retargetable decompiler that performs a program transformation from a machine code into a human-readable form of representation. All of these tools are based on several novel methods defined by the author. According to our experimental results and users feed-back, all of the proposed tools are at least fully competitive to existing solutions, while outperforming these solutions in several ways.
|
|
Harnessing Forest Automata for Verification of Heap Manipulating Programs
Šimáček, Jiří ; Abdulla, Parosh (oponent) ; Křetínský, Mojmír (oponent) ; Vojnar, Tomáš (vedoucí práce)
This work addresses verification of infinite-state systems, more specifically, verification of programs manipulating complex dynamic linked data structures. Many different approaches emerged to date, but none of them provides a~sufficiently robust solution which would succeed in all possible scenarios appearing in practice. Therefore, in this work, we propose a new approach which aims at improving the current state of the art in several dimensions. Our approach is based on using tree automata, but it is also partially inspired by some ideas taken from the methods based on separation logic. Apart from that, we also present multiple advancements within the implementation of various tree automata operations, crucial for our verification method to succeed in practice. Namely, we provide an optimised algorithm for computing simulations over labelled transition systems which then translates into more efficient computation of simulations over tree automata. We also give a new algorithm for checking inclusion over tree automata, and we provide experimental evaluation demonstrating
|
|
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.
|
|
Evolutionary Approach to Synthesis and Optimization of Ordinary and Polymorphic Circuits
Gajda, Zbyšek ; Schmidt, Jan (oponent) ; Zelinka,, Ivan (oponent) ; Sekanina, Lukáš (vedoucí práce)
This thesis deals with the evolutionary design and optimization of ordinary and polymorphic circuits. New extensions of Cartesian Genetic Programming (CGP) that allow reducing of the computational time and obtaining more compact circuits are proposed and evaluated. Second part of the thesis is focused on new methods for synthesis of polymorphic circuits. Proposed methods, based on polymorphic binary decision diagrams and polymorphic multiplexing, extend the ordinary circuit representations with the aim of including polymorphic gates. In order to reduce the number of gates in circuits synthesized using proposed methods, an evolutionary optimization based on CGP is implemented and evaluated. The implementations of polymorphic circuits optimized by CGP represent the best known solutions if the number of gates is considered as the target criterion.
|
host ::
