|
Programs and Algorithms of Numerical Mathematics 15
Vejchodský, Tomáš ; Chleboun, J. ; Přikryl, Petr ; Segeth, Karel ; Šístek, Jakub
The book contains papers presented at the international seminar Programs and algorithms of numerical Mathematics 15 (PANM 15), held in Dolni Maxov, Czech Republic, June 6-11, 2010. It is the fifteen volume in the series of the PANM proceedings. The topics of contributions include numerical methods for fluid flow modelling, the finite element method, a posteriori error estimates, topics from numerical linear atgebra, etc.
|
|
Architektura bezserverových jednostránkových aplikací v jazyku JavaScript
Zikmund, Marian ; Pecinovský, Rudolf (vedoucí práce) ; Suchan, Vladimír (oponent)
Cílem diplomové práce je návrh a vývoj frameworku pro tvorbu moderních jednostránkových aplikací (Single Page Application) v programovacím jazyku JavaScript a popsání tohoto přístupu k vývoji. Součástí práce je taktéž jeho dokumentace pro pohodlnější využití a přizpůsobení. Obsah je rozdělen do osmi kapitol. Po úvodu následuje rešerše informačních zdrojů, představení programovacího jazyka JavaScript a vysvětlení problematiky tvorby jednostránkových aplikací, včetně popisu základních principů jejich fungování, motivace a odůvodnění, kdy a proč je tento přístup vhodný. Práce se primárně zaměřuje na problematiku jednostránkových aplikací, pro jejichž tvorbu je programovací jazyk JavaScript klíčový. Z toho důvodu je mu v práci poskytnuta jedna celá kapitola, je zde rozebrána i jeho historie a role v kontextu ostatních. Následuje přehled obecných vlastností jednostránkových aplikací, analýza aktuálně oblíbených řešení stavějících na knihovně ReactJS, z nichž vyplývají požadavky na vyvíjený framework, jehož tvorbou se zabývá následující kapitola. K vyvinutému frameworku je též vytvořena uživatelská příručka. Praktickým výstupem práce je open source framework pro tvorbu bezserverových jednostránkových aplikací, který lze podle požadavků díky své architektuře a dokumentaci vhodně přizpůsobovat.
|
|
Vícekriteriální hry
Tichá, Michaela ; Dlouhý, Martin (vedoucí práce) ; Lachout, Petr (oponent) ; Čičková, Zuzana (oponent)
Teorie vícekriteriálních her je speciální oblastí z teorie her, kdy jeden či více hráčů mají alespoň dvě výplatní funkce a chtějí je maximalizovat zároveň. V této práci je představena řada nových poznatků. Je zkoumán koncept hledání rovnovážných bodů v ryzích strategiích v nekooperativní vícekriteriální hře. Ukázalo se, že je možné určit všechny rovnovážné body v ryzích strategiích úplným prohledáním a vyřešením dvou lineárních programů pro každý bod. Dále je obecně formulováno, jak pomocí dvou lineárních programů ověřit, zda je libovolně navržený bod rovnovážným bodem hry či nikoli. V nekooperativních hrách je také představen koncept, který při znalosti rovnovážného bodu dvoumaticové hry určí preference hráčů, které musejí mít, aby daný bod byl rovnovážným. Přestože hledání rovnovážného bodu dvoumaticové hry je nelineární úloha, hledání preferencí hráčů při znalosti rovnovážného bodu je úloha lineární. Poslední poznatkem v části nekooperativních her je zobecnění konceptu, který vyřeší vícekriteriální hru přiřazením vah jednotlivým kritériím každým hráčem. V práci je dokázáno, že se nemusí jednat nutně o lineární váhy, ale pro řešení převedením na jednokriteriální hru stačí obecnější funkce, kterou hráč popíše své preference. Zbylá část práce se věnuje poznatkům v kooperativních hrách. V práci se uvažuje, že hráči znají své preference a jsou schopni je vyjádřit pomocí vah. Hra se známými preferencemi je definována a vyřešena za pomoci teorie vyjednávání. Poté je ještě zobecněna na případ, kdy hráči nejen že mají více kritérií, ale mají také více výplatních funkcí, ze kterých si mohou vybrat na základě svého uvážení. Nakonec je definován vícekriteriální případ speciálního typu kooperativní hry - volební hry. Je navržen zcela nový koncept, který vybere vítěznou koalici ve volební hře. Ten je poté aplikován na reálnou situaci po volbách do Poslanecké sněmovny Parlamentu ČR v roce 2013.
|
|
Požadavky podniků na profil absolventa – softwarového vývojáře
Trnková, Michaela ; Pecinovský, Rudolf (vedoucí práce) ; Pavlíčková, Jarmila (oponent)
Předmětem bakalářské práce je zmapování požadavků, které jsou kladeny na absolventy - softwarové vývojáře. Cíle je dosaženo pomocí rozhovorů s odborníky z praxe. Důležitou částí práce je zhodnocení různých metodik výuky programování s blížším zaměřením na metodiku. Přístupy jsou zhodnoceny z pohledu zástupců podniků, učitelů programování a obdobných předmětů na vysokých školách i studentů informatických oborů. Hlavním přínosem práce je souhrn doporučení pro školy pro výuku studentů, která vyplývají z názorů vývojářů a vedoucích vývojářských týmů z technologických firem a názorů studentů, kteří předměty programování absolvovali. Práce obsahuje i doporučení pro studenty, kteří se chtějí v budoucnu zabývat vývojem softwaru.
|
|
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í.
|
|
Význam komprehensivní rehabilitace u pacientů s roztroušenou sklerózou mozkomíšní
Keclíková, Lucie ; Malá, Michaela (oponent) ; Hošková, Blanka (vedoucí práce)
2 Souhrn: Název práce: Význam komprehensivní rehabilitace u pacientů s roztroušenou sklerózou mozkomíšní Cíl práce: Shrnout obecné poznatky o roztroušené skleróze mozkomíšní. Charakterizovat komprehensivní rehabilitaci s důrazem na složku léčebné rehabilitace (zaměřit se na možnosti pohybových aktivit i jednotlivých speciálních terapeutických postupů) a popsat její význam u pacientů s roztroušenou sklerózou mozkomíšní. Na základě teoretických poznatků stanovit 12 ti týdenní komplexní rehabilitační program a vyzkoušet jeho účinnost v praxi. Metoda: Z metod výzkumu byla použita varianta experiment, metoda komparace a dotazníková metoda. Byl hodnocen účinek 12ti týdenního komplexního rehabilitačního programu u dvou stejně početných souborů (n = 10) pacientů s RS (EDSS 1-5) vybraných z databáze Centra pro demyelinizační onemocnění neurologické kliniky VFN a 1.LF UK pomocí chodeckého testu (T25- FW), Kurtzkeho stupnice postižení (EDSS), dotazníků dopadu únavy (MFIS), kvality života nemocných RS (MSQOL-54) a určení limitu aktivity a restrikce participace (WHODAS II). První soubor tvořila experimentální skupina, která absolvovala 12 ti týdenní komplexní rehabilitační program. V případě druhého souboru šlo o kontrolní skupinu vybraných pacientů, kteří neprováděli žádnou část z tohoto programu po stejné časové...
|
|
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.
|
host ::
