|
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.
|
|
Důvěra a reputace v distribuovaných systémech
Samek, Jan ; Návrat,, Pavol (oponent) ; Šafařík,, Jiří (oponent) ; Hanáček, Petr (vedoucí práce)
Tato disertační práce se zabývá problematikou modelování důvěry v distribuovaných systémech, konkrétně pak více-kontextové důvěry v distribuovaných multi-agentních systémech. V současné době existuje velké množství modelů důvěry či reputace, nicméně více-kontextová vlastnost důvěry či reputace v nich není často zohledněna. Z tohoto důvodu se práce zaměřuje především na analýzu více-kontextových modelů založených na důvěře a na jejím základě stanovuje předpoklady pro nový, vlastnost více-kontextovost plně podporující, model důvěry. Stěžejní částí práce je formální návrh nového více-kontextového modelu důvěry, který je schopen vytvářet, aktualizovat a uchovávat důvěru pro různé aspekty (kontexty) jedné entity multi-agentního systému. Důvěru lze v navrženém modelu budovat jak na základě přímých zkušeností, tak i na základě doporučení a reputace. Dalším aspektem navrženého modelu je schopnost odvozovat důvěru v různé kontexty na základě znalosti důvěry v kontexty jiné, což je zajištěno vytvořením hierarchické struktury jednotlivých kontextů jedné entity. Přínosem nového modelu je především zvýšení efektivity rozhodování agentů v rámci multi-agentního systému ve smyslu schopnosti výběru optimálního partnera pro provedení transakce. Návrh modelu byl ověřen implementací prototypu multi-agentního systému, ve kterém se agenti rozhodují a jednají na základě důvěry.
|
|
Acceleration Methods for Evolutionary Design of Digital Circuits
Vašíček, Zdeněk ; Miller, Julian (oponent) ; Zelinka,, Ivan (oponent) ; Sekanina, Lukáš (vedoucí práce)
Although many examples showing the merits of evolutionary design over conventional design techniques utilized in the field of digital circuits design have been published, the evolutionary approaches are usually hardly applicable in practice due to the various so-called scalability problems. The scalability problem represents a general problem that refers to a situation in which the evolutionary algorithm is able to provide a solution to a small problem instances only. For example, the scalability of evaluation of a candidate digital circuit represents a serious issue because the time needed to evaluate a candidate solution grows exponentially with the increasing number of primary inputs. In this thesis, the scalability problem of evaluation of a candidate digital circuit is addressed. Three different approaches to overcoming this problem are proposed. Our goal is to demonstrate that the evolutionary design approach can produce interesting and human competitive solutions when the problem of scalability is reduced and thus a sufficient number of generations can be utilized. In order to increase the performance of the evolutionary design of image filters, a domain specific FPGA-based accelerator has been designed. The evolutionary design of image filters is a kind of regression problem which requires to evaluate a large number of training vectors as well as generations in order to find a satisfactory solution. By means of the proposed FPGA accelerator, very efficient nonlinear image filters have been discovered. One of the discovered implementations of an impulse noise filter consisting of four evolutionary designed filters is protected by the Czech utility model. A different approach has been introduced in the area of logic synthesis. A method combining formal verification techniques with evolutionary design that allows a significant acceleration of the fitness evaluation procedure was proposed. The proposed system can produce complex and simultaneously innovative designs, overcoming thus the major bottleneck of the evolutionary synthesis at gate level. The proposed method has been evaluated using a set of benchmark circuits and compared with conventional academia as well as commercial synthesis tools. In comparison with the conventional synthesis tools, the average improvement in terms of the number of gates provided by our system is approximately 25%. Finally, the problem of the multiple constant multiplier design, which belongs to the class of problems where a candidate solution can be perfectly evaluated in a short time, has been investigated. We have demonstrated that there exists a class of circuits that can be evaluated efficiently if a domain knowledge is utilized (in this case the linearity of components).
|
|
Multimedia Data Processing in Heterogeneous Distributed Environment
Kajan, Rudolf ; Ferko,, Andrej (oponent) ; Míkovec, Zdeněk (oponent) ; Herout, Adam (vedoucí práce)
Ubiquitous computing, a paradigm in which the processing of information is linked with each activity or object as encountered, was proposed by Mark Weiser as the next era for interacting with computers. Its goal is to enable people to interact with devices more naturally and casually in ways that suit whatever location or context they find themselves in. Ubiquitous computing focuses on learning by removing the complexity of computing and increases efficiency while using computing for different daily activities. But after more than 15 years since Weiser formulated these goals, several aspects of ubiquitous computing are still not a part of user experience with today’s technology. Seamless integration with environment leading to technological invisibility or user interaction spanning across multiple devices pose still a great challenge. The main goal of our work is to make a step towards making the idea of ubiquitous computing a reality by addressing the question about intuitive information sharing between a personal device and a situated display. We have developed three interaction techniques which support unobtrusive content exchange between touch-enabled personal device and a large display - whether it is shared-private or public. These techniques are based on video streams, augmented reality, and analysis of gaze data. Besides the interaction techniques, we also present a framework for real-time application state acquisition and reconstruction on target platform. We report on user studies focused on the usability of our prototypes and a system performance evaluations. Our experiments were formed around real-life scenarios which are commonly experienced throughout the day. For interactions based on video streams, the results indicate that our techniques outperform the existing solutions: the localization and task migration is done in real time on a midlevel cellphone; the localization is reliable even for different observation angles and for cluttered screen content. Our technique based on gaze analysis goes even further by allowing for modeling of implicit user preferences through gaze data, while being accurate and unobtrusive.
|
|
Právní a zdravotně sociální aspekty činnosti OSPOD jako ustanovených opatrovníků v zámu nezletilých dětí
BORSKÁ, Jana
Česká republika, jako signatář Úmluvy o právech dítěte, svěřila výkon státní správy na úseku péče o nezletilé děti obecním úřadům obcí s rozšířenou působností, kde ochranu práv a oprávněných zájmů nezletilých dětí vykonávají orgány sociálně právní ochrany dětí (dále jen OSPOD), které jsou začleněny do systému výkonu státní správy v územním členění tak, aby byla zajištěna komplexní péče o nezletilé děti v rozsahu stanoveném zákonem o sociálně právní ochraně dětí. Postavení a úloha OSPOD, který je pověřen výkonem státní správy na úseku ochrany nezletilých dětí, jsou upraveny zák. č. 359/1999 Sb., o sociálně právní ochraně dětí, v platném znění. Stejně důležité je zakotvení postavení lidí pracujících na těchto úřadech. Z hlediska odbornosti jsou na ně kladeny vysoké nároky z hlediska znalostního profilu zejména z oboru práva. Jedná se o velice náročnou práci, která klade vysoké nároky na osobnostní profil zaměstnance. ČR provedla v posledních třech letech rozsáhlé zásahy do právní úpravy problematiky sociálně právní ochrany dětí, kde došlo k posílení ochrany práv nezletilých dětí a stanovení nových nástrojů k jejich ochraně. Přijetím nové právní úpravy rodinného práva, které je komplexně upraveno v zák. č. 89/2012 Sb., občanském zákoníku, následovala nová právní úprava procesních předpisů spojených s ochranou práv nezletilých dětí, kde vedle zák. č. 99/1963, občanský soudní řád platí také zák. č. 292/2013 Sb., o zvláštních řízeních soudních. Rozhodování o nezletilých dětech stát svěřil převážně do pravomoci soudů, které jmenují místně příslušný OSPOD opatrovníkem k zastupování zájmů nezletilých dětí. Na základě provedeného rozboru základních pojmů bylo cílem zjistit názory vybraných vedoucích pracovníků OSPOD a soudců okresních soudů na vydefinované problémy vyskytující se v postupech činnosti OSPOD a soudů při ochraně zájmu nezletilých dětí. Ve výzkumné části práce byly rozborem kazuistik vytipovány problémy v činnosti OSPOD. Z návrhů soudců i vedoucích pracovníků OSPOD vyplynula nezbytnost sjednocení místní příslušnosti. Soudy navrhují sjednocení dle místa, kde se nezletilé dítě zdržuje; OSPOD dle místa trvalého pobytu. Všech 10 oslovených vedoucích pracovníků OSPOD označilo za problém dožádání, kde tento institut není zahrnut do hodnocení výkonů, nelze jej odmítnout. Podjatost činí problémy v různých fázích řízení - je zde patrný rozdílný přístup soudů k řešení dané problematiky (některé vznesenou námitku podjatosti u soudu řeší a jiní nikoliv) a pro pracovníky OSPOD je obtížné odhadnout - jak se zachovat, je-li vůči nim námitka podjatosti vznesena (z tohoto důvodu bylo téma "podjatosti zpracováno komplexně včetně výkladu právního postupu pro pracovníky OSPOD). Vzdělávání pracovníků OSPOD je zákonem stanovenou povinností. Ne všem OSPOD se daří zajistit školení v požadovaném rozsahu - a to z finančních důvodů (průměrné náklady na školení na jednoho zaměstnance je od 9167,-- do 13400 Kč ročně - tyto náklady odpovídají cca 6 dnům školení). Pracovní vytíženost způsobená nedostatečným počtem zaměstnanců OSPOD neumožňuje absolvovat tato povinná školení. V rámci zkoumání "účasti kolizního opatrovníka při jednání u soudu" bylo zjištěno - nepravidelná účast kolizního opatrovníka u soudu (neúčast při odvolacím řízení); nedostatek zkušeností pracovníků OSPOD v této oblasti; neúplné zprávy z šetření v rodině, které jsou určené pro soud. Na základě vyhodnocení rozhovorů vyplynuly návrhy na zlepšení organizace školení OSPOD, na základě povedeného komplexního rozboru řešení problematiky místní příslušnosti bylo doporučeno řešení samostatné evidence dožádání a finanční kompenzace činnosti OSPOD při dožádání provedení zastupování nezletilých u soudu, vypracování návrhů předběžných opatření, návrh možného řešení začlenění OSPOD v jiné organizační struktuře.
|
|
Měření fonologického povědomí – test skládání hlásek na počátku školní docházky: porovnání klasického přístupu a teorie odpovědi na položku
Gorčíková, M. ; Šafr, Jiří
Cílem příspěvku je ukázat výhody a limity dvou přístupů klasické teorie měření (CCT) a teorie odpovědi na položku (IRT) k posouzení úrovně diagnostického nástroje pro hodnocení fonologického povědomí (FP) mezi žáky prvních tříd. FP bylo měřeno testem skládání hlásek v rámci longitudinálního výzkumu 25 škol v Praze a Středočeském kraji (N=439). Výhodou přístupu IRT oproti klasické testové teorie je především pojetí nezávislosti položek v testu. Pravděpodobnost určité odpovědi je tak závislá na úrovni latentní schopnosti žáka a charakteristikách konkrétní položky. Pokud tedy známe parametry položek (obtížnost) lze na základě odpovědí žáka odhadnout úroveň měřené lingvistické schopnosti uplatnitelné v praktické diagnostice. Výsledky poukázaly na vhodnost úpravy testu skládání hlásek (zejména pro konec první třídy) tak, aby adekvátně měřil velkou dynamiku růstu úrovně schopnosti FP během první třídy.
|
|
Dopad obecného nařízení o ochraně osobních údajů na šedou literaturu
Koščík, Michal
V dubnu 2016 bylo přijato nové obecné nařízení o ochraně osobních údajů, jež v zásadních principech vychází ze stávající právní úpravy, v mnohém ji však rozvádí a konkretizuje. Příspěvek má převážně přehledový charakter a zaměří se na novou úpravu povinností, jimž se budou muset správci repozitářů v horizontu nejbližších dvou let přizpůsobit. Příspěvek bude věnován zejména otázkám souhlasu se zpracováním údajů, informovanosti subjektu údajů, přebírání osobních údajů od třetích stran, možnostech zpracovávat a zveřejňovat některé osobní údaje i bez souhlasu dotčených osob a nově formulovanému právu být zapomenut.
Plný text: idr-1039_1 -  PDF
Prezentace: idr-1039_2 - PDF; idr-1039_3 - PDF
Videozáznam: idr-1039_4 -  MP4
|
|
Proměny agrární krajiny mikroregionu Sedlčanska v letech 1850-1943
Mašková Janotová, Šárka ; Jakubec, Ivan (vedoucí práce) ; Štemberk, Jan (oponent)
Práce je zaměřena na vývoj hospodářské situace oblasti Sedlčanska od první poloviny 19. století až po 2. polovinu století 20. Tímto obdobím je vyměřen prostor pro sledování proměn z počátku ryze agrární (zemědělské) krajiny v krajinu, jež by na konci 2. republiky mohla být označena krajinou agrárně průmyslovou. Území Sedlčanska bývá tradičně pojímáno jako území průmyslově "retardované". Předkládaná práce se proto snaží zjistit na kolik jde o představu pravdivou, zdali zde v daném období neexistovala ohniska dynamického hospodářského rozvoje a existovala-li, nakolik byla srovnatelná s hospodářským rozvojem zbylých Čech. Přičemž se snaží poukázat na důvody, které ke vzniku dané situace vedly. Zasazuje tedy regionální stav do širších souvislostí industrializace Českých zemí ve vymezeném časovém období. Fenomén industrializace samozřejmě přímo souvisí s faktory jakými jsou demografický vývoj, doprava, obchod, peněžnictví, zemědělství a správní činnost. Tyto aspekty proměny hospodářské situace Sedlčanska jsou proto v práci zohledněny a zmapovány. Sledována je také spolková činnost v dané oblasti. Přičemž jde o spolky, které si kladou za cíl právě hospodářský rozvoj této krajiny a které zdůrazňují především vzestup rolnického stavu. Klíčová slova Sedlčansko, hospodářské dějiny, industrializace, zemědělství
|
|
Marketing nákupního centra
POLÁKOVÁ, Lucie
Předložená diplomová práce pojednává o nově otevřeném nákupním centru Galerie v Teplicích, které v současné době usiluje o vybudování výhodné pozice na trhu a rovněž pracuje na svém vhodném vymezení vůči stávající silné konkurenci. Hlavními cíli této práce je zjistit, jakou pozici výše zmíněné nákupní centrum v současné době na trhu zaujímá, poznat blíže jeho návštěvníky a následně na základě výsledků realizovaných šetření lépe zacílit a přizpůsobit stávající marketingovou komunikaci centra. Z tohoto důvodu je tato diplomová práce zaměřená zejména na zjišťování a analýzu bližších informací o chování, vnímání a preferencích návštěvníků určených nákupních center, především pak nákupního centra Galerie a rovněž na vymezení jeho současného positioningu ve vztahu k určeným konkurentům.
|
|
Vzdělávání a rozvoj zaměstnanců ve vybrané organizaci
MILCOVÁ, Kristýna
Cílem této diplomové práce je analyzovat proces vzdělávání a rozvoje zaměstnanců, charakterizovat a zhodnotit stávající personální procesy, identifikovat potřeby zaměstnanců a podniku a navrhnout možné způsoby zlepšení stávající situace. Pro tento účel byla vybrána společnost Fabory CZ Holding s.r.o.
|
host ::
