|
Relational Verification of Programs with Integer Data
Konečný, Filip ; Bouajjani, Ahmed (referee) ; Jančar, Petr (referee) ; Vojnar, Tomáš (advisor)
Tato práce představuje nové metody pro verifikaci programů pracujících s neomezenými celočíslenými proměnnými, konkrétně metody pro analýzu dosažitelnosti a~konečnosti. Většina těchto metod je založena na akceleračních technikách, které počítají tranzitivní uzávěry cyklů programu. V práci je nejprve představen algoritmus pro akceleraci několika tříd celočíselných relací. Tento algoritmus je až o čtyři řády rychlejší než existující techniky. Z teoretického hlediska práce dokazuje, že uvažované třídy relací jsou periodické a~poskytuje tudíž jednotné řešení prolému akcelerace. Práce dále představuje semi-algoritmus pro analýzu dosažitelnosti celočíselných programů, který sleduje relace mezi proměnnými programu a~aplikuje akcelerační techniky za účelem modulárního výpočtu souhrnů procedur. Dále je v práci navržen alternativní algoritmus pro analýzu dosažitelnosti, který integruje predikátovou abstrakci s accelerací s cílem zvýšit pravděpodobnost konvergence výpočtu. Provedené experimenty ukazují, že oba algoritmy lze úspěšně aplikovat k verifikaci programů, na kterých předchozí metody selhávaly. Práce se rovněž zabývá problémem konečnosti běhu programů a~dokazuje, že tento problém je rozhodnutelný pro několik tříd celočíselných relací. Pro některé z těchto tříd relací je v práci navržen algoritmus, který v polynomiálním čase vypočítá množinu všech konfigurací programu, z nichž existuje nekonečný běh. Tento algoritmus je integrován do metody, která analyzuje konečnost běhů celočíselných programů. Efektivnost této metody je demonstrována na několika netriviálních celočíselných programech.
|
|
Trust and Reputation in Distributed Systems
Samek, Jan ; Návrat,, Pavol (referee) ; Šafařík,, Jiří (referee) ; Hanáček, Petr (advisor)
This Ph.D. thesis deals with trust modelling for distributed systems especially to multi-context trust modelling for multi-agent distributed systems. There exists many trust and reputation models but most of them do not dealt with the multi-context property of trust or reputation. Therefore, the main focus of this thesis is on analysis of multi-context trust based models and provides main assumptions for new fully multi-contextual trust model on the bases of them. The main part of this thesis is in providing new formal multi-context trust model which are able to build, update and maintain trust value for different aspects (contexts) of the single entity in the multi-agent system. In our proposal, trust value can be built on the bases of direct interactions or on the bases on recommendations and reputation. Moreover we assume that some context of one agent is not fully independent and on the bases of trust about one of them we are able to infer trust to another's. Main contribution of this new model is increasing the efficiency in agent decision making in terms of optimal partner selection for interactions. Proposed model was verified by implementing prototype of multi-agent system when trust was used for agents' decision making and acting.
|
|
Acceleration Methods for Evolutionary Design of Digital Circuits
Vašíček, Zdeněk ; Miller, Julian (referee) ; Zelinka,, Ivan (referee) ; Sekanina, Lukáš (advisor)
Ačkoliv můžeme v literatuře nalézt řadu příkladů prezentujících evoluční návrh jakožto zajímavou a slibnou alternativu k tradičním návrhovým technikám používaným v oblasti číslicových obvodů, praktické nasazení je často problematické zejména v důsledku tzv. problému škálovatelnosti, který se projevuje např. tak, že evoluční algoritmus je schopen poskytovat uspokojivé výsledky pouze pro malé instance řešeného problému. Vážný problém představuje tzv. problém škálovatelnosti evaluace fitness funkce, který je markantní zejména v oblasti syntézy kombinačních obvodů, kde doba potřebná pro ohodnocení kandidátního řešení typicky roste exponenciálně se zvyšujícím se počtem primárních vstupů. Tato disertační práce se zabývá návrhem několika metod umožňujících redukovat problem škálovatelnosti evaluace v oblasti evolučního návrhu a optimalizace číslicových systémů. Cílem je pomocí několika případových studií ukázat, že s využitím vhodných akceleračních technik jsou evoluční techniky schopny automaticky navrhovat inovativní/kompetitivní řešení praktických problémů. Aby bylo možné redukovat problém škálovatelnosti v oblasti evolučního návrhu číslicových filtrů, byl navržen doménově specifický akcelerátor na bázi FPGA. Tato problematika reprezentuje případ, kdy je nutné ohodnotit velké množství trénovacích dat a současně provést mnoho generací. Pomocí navrženého akcelerátoru se podařilo objevit efektivní implementace různých nelineárních obrazových filtrů. S využitím evolučně navržených filtrů byl vytvořen robustní nelineární filtr implusního šumu, který je chráněn užitným vzorem. Navržený filtr vykazuje v porovnání s konvenčními řešeními vysokou kvalitu filtrace a nízkou implementační cenu. Spojením evolučního návrhu a technik známých z oblasti formální verifikace se podařilo vytvořit systém umožňující výrazně redukovat problém škálovatelnosti evoluční syntézy kombinačních obvodů na úrovni hradel. Navržená metoda dovoluje produkovat komplexní a přesto kvalitní řešení, která jsou schopna konkurovat komerčním nástrojům pro logickou syntézu. Navržený algoritmus byl experimentálně ověřen na sadě několika benchmarkových obvodů včetně tzv. obtížně syntetizovatelných obvodů, kde dosahoval v průměru o 25% lepších výsledků než dostupné akademické i komerční nástroje. Poslední doménou, kterou se práce zabývá, je akcelerace evolučního návrhu lineárních systémů. Na příkladu evolučního návrhu násobiček s vícenásobnými konstantními koeficienty bylo ukázáno, že čas potřebný k evaluaci kandidátního řešení lze výrazně redukovat (defacto na ohodocení jediného testovacího vektoru), je-li brán v potaz charakter řešeného problému (v tomto případě linearita).
|
|
Multimedia Data Processing in Heterogeneous Distributed Environment
Kajan, Rudolf ; Ferko,, Andrej (referee) ; Míkovec, Zdeněk (referee) ; Herout, Adam (advisor)
Pervasive computing sa zameriava odstránenie zložitostí pri interakcii s výpočtovou technikou a zvýšenie efektivity pri jej každodennom používaní. Ale i po viac ako 15 rokoch od sformulovania hlavných cieľov Pervasive computingu existujú aspekty interakcie ktoré stále nie sú súčasťou užívateľskej skúsenosti s dnešnou technológiou. Bezproblémová integrácia s prostredím vedúca k technologickej neviditeľnosti, alebo interakcia naprieč rôznymi zariadeniami predstavujú stále veľkú výzvu. Hlavným cieľom tejto práce je prispieť k tomu, aby sa ciele Pervasive computingu priblížili k realizovaniu tým, že predstavíme spôsob intuitívneho zdieľania informácií medzi osobným a verejne umiestneným zariadením. Predstavili sme tri interakčné techniky, ktoré podporujú intuitívnu výmenu obsahu medzi osobným zariadením a zdieľaným displejom. Tieto techniky sú založené na prenose videa, rozšírenej realite a analýze pohľadových dát. Okrem interakčných techník sme tiež predstavili mechanizmus pre získavanie, prenos a rekonštrukciu aplikačného stavu na cieľovom zariadení.
|
|
Právní a zdravotně sociální aspekty činnosti OSPOD jako ustanovených opatrovníků v zámu nezletilých dětí
BORSKÁ, Jana
The Czech Republic as a signatory of the Convention on the Rights of the Child has vested the practice of state administration in the field of care for minor children to municipalities with extended powers, where the protection of the rights and legitimate interests of minor children is safeguarded by state authorities of social and legal protection of children (ASLPC hereinafter). These authorities are incorporated to the extent laid down by the Act on Social and Legal Protection of Children (Act No 359/1999 Coll., as amended). The position and roles of ASLPC and their competence and jurisdiction are also regulated by the same act. The position of workers of these authorities and its legal embodiment is equally important. Regarding professionality, there are high demands on these workers. In the Czech Republic, significant changes in legislature have been made over the past three years. These amendments have led to the strengthening of the rights of minor children and to the establishing of new tools for their protection. In connection with the adoption of new substantive regulation of family law, which is now exhaustively dealt with by the Act No 89/2012 Coll., the Civil Code, new procedural rules have been established regarding protection of rights of minor children. Such procedural legislation includes (apart from the long-existent Act No. 99/1963, the Code of Civil Procedure) the Act No 292/2013 Coll., on Special Civil Proceedings. The decision-making regarding minor children has been vested mainly by the state into the competence of courts. The courts appoint the locally relevant ASLPC as a guardian who then represents the interests of minor children. The purpose, interwoven with and derived from the first one, was to explore the opinions of selected social workers of ASLPC and of district court judges regarding the defined problems occurring during the work of ASLPCs and courts while protecting the interests of minor children. These particularly include: the use of the tool of precautionary measure; problems of different territorial jurisdiction of courts and ASLPCs; processing of complaints regarding bias in various phases of the proceedings; professional training of workers of ASLPC It is evident from the proposals of both judges and ASLPC workers that it is necessary to unify territorial jurisdiction. The courts are suggesting the priority criterion of the address where the child mainly resides. ASLPC workers suggest the official permanent residence as the prime criterion. Bias causes problems in all phases of proceedings. It is obvious that courts take differing approaches towards the solution of this problem (some courts solve the problem of bias complaints filed by the parties while other courts do not) and for ASLPC workers it is difficult to assess how to act when such complaint is raised against them. The training of ASLPC workers - workers are obliged to educate themselves and their employer is obliged to finance such training. Not all ASLPCs are able to provide training in the required extent - due to financial reasons (the average costs of education of one employee pose from 9,169 to 13,400 CZK annually and they cover approximately 6 days of training). The heavy work-load caused by insufficient numbers of ASLPC employees prevents them from completing such compulsory training. As part of the examination of the "participation of a collision guardian in court proceedings" it has been found out that irregular participation of the worker in the proceedings (absence from participation in appeals proceedings); incomplete reports (directed to courts) from surveys in families. Based on comprehensive examination of the problems of territorial jurisdiction, it was recommended that requests are independently recorded and financial compensation is provided for ASLPCs who are requested to represent minors in front of courts, to draft proposals for precautionary measures.
|
|
Measuring phonological awareness – blend phoneme test in the beginning of schooling: an comparison of classical test theory and item response theory
Gorčíková, M. ; Šafr, Jiří
The main purpose of this paper is to show dis/advantages of two approaches classical test theory (CTT) and item response theory (IRT) to assess the level of diagnostic tools for evaluating phonemic awareness among first-grade students using longitudinal survey of children during the first grade of primary school (25 schools in Prague and Central Bohemia, 439 pupils). Phonemic awareness (FA) was measured by the task blend phonemes into syllables and words. The advantage of IRT compared to CTT is primarily a concept of independence of the test items. The probability of a response is dependent on the level of latent ability and characteristics of items. So if we know the characteristic of items parameter (difficulty) it could be estimated from the pupil´s responses the level of language skill for diagnostics. The results showed the need for blend phoneme test modifications (in particular for the end of the first grade) so as to adequately measure the high growth of FA ability levels during the first grade.
|
|
General Data Protection Regulation and its Impact on Grey Literature
Koščík, Michal
In April 2016, the European commission adopted a new General Data Protection Regulation. This regulation is based on fundamental principles of the existing legislation and elaborates it further into the set of rather detailed legal instructions. The suggested paper aims to summarize the parts of the new regulation that are most relevant for operators of gray literature repositories, who will have to adapt within the next two years. The paper will focus on the issues of consent to the processing of personal data, the legal regime of processing personal data without the consent of the data subjects, the data subject’s right to information as well as the legal regime of acquisition of personal data by third parties and exercise of the newly formulated right to be forgotten.
Fulltext: idr-1039_1 -  PDF
Slides: idr-1039_2 - PDF; idr-1039_3 - PDF
Video: idr-1039_4 -  MP4
|
|
The Changes of agricultural Landscape of Microregion Sedlčany in the years 1850-1943
Mašková Janotová, Šárka ; Jakubec, Ivan (advisor) ; Štemberk, Jan (referee)
The thesis is focused on the economic situation development in the Sedlčany region from the first half of the 19th century till second half of the 20th century. The period observes changes from the agrarian landscape. At the end of period of the Second Czechoslovak Republic the landscape could be described as agrarian-industrial landscape. Traditionally, the Sedlčany region is considered industrially influenced. The presented thesis deals with confirmation or disproof of this idea. The research tries to find the potential focuses of dynamic economic development. If the focuses existed in the past, the research deals with comparison economic development of the Sedlčany region with other parts of Bohemia and finds the circumstances of the development. The economic situation of this area is located into wider context of the industrialization in the Czech countries during given period. Of course, the phenomenon of industrialization process relates to many factors, such as demographic development, transportation, trade, banking, agriculture and administrative activities. The federation actions are followed up in the region. The main aim of the associations is economic development of this region. They emphasize mainly upward movement of the peasant status. Keywords Sedlčany, economic history,...
|
|
Marketing at the shopping centre
POLÁKOVÁ, Lucie
The presented diploma thesis deals with the newly opened shopping center Galerie Teplice. The center is currently working on creation of a suitable market position with respect to the existing strong competition. The objective of the thesis is to evaluate the current position of the aforementioned shopping center on the market, then to learn more about its visitors and finally to improve targeting and personalize the marketing communication based on the analysis of results. For this reason the diploma thesis is focused on identifying and analyzing detailed information about the behavior, perceptions and preferences of visitors of designated shopping centers, especially of the Galerie center and on defining of its current positioning in relation to specified competitors.
|
| |
guest ::
