|
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.
|
|
Extensions to Probabilistic Linear Discriminant Analysis for Speaker Recognition
Plchot, Oldřich ; Fousek, Petr (referee) ; McCree,, Alan (referee) ; Burget, Lukáš (advisor)
Tato práce se zabývá pravděpodobnostními modely pro automatické rozpoznávání řečníka. Podrobně analyzuje zejména pravděpodobnostní lineární diskriminační analýzu (PLDA), která modeluje nízkodimenzionální reprezentace promluv ve formě \acronym{i--vektorů}. Práce navrhuje dvě rozšíření v současnosti požívaného PLDA modelu. Nově navržený PLDA model s plným posteriorním rozložením modeluje neurčitost při generování i--vektorů. Práce také navrhuje nový diskriminativní přístup k trénování systému pro verifikaci řečníka, který je založený na PLDA. Pokud srovnáváme původní PLDA s modelem rozšířeným o modelování neurčitosti i--vektorů, výsledky dosažené s rozšířeným modelem dosahují až 20% relativního zlepšení při testech s krátkými nahrávkami. Pro delší testovací segmenty (více než jedna minuta) je zisk v přesnosti menší, nicméně přesnost nového modelu není nikdy menší než přesnost výchozího systému. Trénovací data jsou ale obvykle dostupná ve formě dostatečně dlouhých segmentů, proto v těchto případech použití nového modelu neposkytuje žádné výhody při trénování. Při trénování může být použit původní PLDA model a jeho rozšířená verze může být využita pro získání skóre v případě, kdy se bude provádět testování na krátkých segmentech řeči. Diskriminativní model je založen na klasifikaci dvojic i--vektorů do dvou tříd představujících oprávněný a neoprávněný soud (target a non-target trial). Funkcionální forma pro získání skóre pro každý pár je odvozena z PLDA a trénování je založeno na logistické regresi, která minimalizuje vzájemnou entropii mezi správným označením všech soudů a pravděpodobnostním označením soudů, které navrhuje systém. Výsledky dosažené s diskriminativně trénovaným klasifikátorem jsou podobné výsledkům generativního PLDA, ale diskriminativní systém prokazuje schopnost produkovat lépe kalibrované skóre. Tato schopnost vede k lepší skutečné přesnosti na neviděné evaluační sadě, což je důležitá vlastnost pro reálné použití.
|
|
Sharing Local Information for Faster Scanning-Window Object Detection
Hradiš, Michal ; Kälviäinen, Heikki (referee) ; Matas, Jiří (referee) ; Zemčík, Pavel (advisor)
Cílem této dizertační prace je vylepšit existující detektory objektů pomocí sdílení informace a výpočtů mezi blízkými pozicemi v obraze. Navrhuje dvě metody, které jsou založené na Waldově sekvenčním testu poměrem pravděpodobností a algoritmu WaldBoost. První z nich, Early non-Maxima Suppression , přesunuje rozhodování o potlačení nemaximálních pozic ze závěrečné fáze do fáze vyhodnocování detektoru, čímž zamezuje zbytečným výpočtům detektoru v nemaximálních pozicích. Metoda neighborhood suppression doplňuje existující detektory o schopnost zavrhnout okolní pozice v obraze. Navržené metody je možné aplikovat na širokou škálu detektorů. Vyhodnocení obou metod dokazují jejich výrazně vyšší efektivitu v porovnání s detektory, které vyhodnocují jednotlivé pozice obrazu zvlášť. Dizertace navíc prezentuje výsledky rozsáhlých experimentů, jejichž cílem bylo vyhodnotit vlastnosti běžných obrazových příznaků v několika detekčních úlohách a situacích.
|
|
Query-by-Example Spoken Term Detection
Fapšo, Michal ; Matoušek, Jindřich (referee) ; Metze, Florian (referee) ; Černocký, Jan (advisor)
Tato práce se zabývá vyhledáváním výrazů v řeči pomocí mluvených příkladů (QbE STD). Výrazy jsou zadávány v mluvené podobě a jsou vyhledány v množině řečových nahrávek, výstupem vyhledávání je seznam detekcí s jejich skóre a časováním. V práci popisujeme, analyzujeme a srovnáváme tři různé přístupy ke QbE STD v jazykově závislých a jazykově nezávislých podmínkách, s jedním a pěti příklady na dotaz. Pro naše experimenty jsme použili česká, maďarská, anglická a arabská (levantská) data, a pro každý z těchto jazyků jsme natrénovali 3-stavový fonémový rozpoznávač. To nám dalo 16 možných kombinací jazyka pro vyhodnocení a jazyka na kterém byl natrénovaný rozpoznávač. Čtyři kombinace byly tedy závislé na jazyce (language-dependent) a 12 bylo jazykově nezávislých (language-independent). Všechny QbE systémy byly vyhodnoceny na stejných datech a stejných fonémových posteriorních příznacích, pomocí metrik: nesdružené Figure-of-Merit (non pooled FOM) a námi navrhnuté nesdružené Figure-of-Merit se simulací normalizace přes promluvy (utterrance-normalized non-pooled Figure-of-Merit). Ty nám poskytly relevantní údaje pro porovnání těchto QbE přístupů a pro získání lepšího vhledu do jejich chování. QbE přístupy použité v této práci jsou: sekvenční statistické modelování (GMM/HMM), srovnávání vzorů v příznacích (DTW) a srovnávání grafů hypotéz (WFST). Abychom porovnali výsledky QbE přístupů s běžnými STD systémy vyhledávajícími textové výrazy, vyhodnotili jsme jazykově závislé konfigurace také s akustickým detektorem klíčových slov (AKWS) a systémem pro vyhledávání fonémových řetězců v grafech hypotéz (WFSTlat). Jádrem této práce je vývoj, analýza a zlepšení systému WFST QbE STD, který po zlepšení dosahuje podobných výsledků jako DTW systém v jazykově závislých podmínkách.
|
|
The Pump with a Diffuser with Stochastic Blades (Runner and Diffuser)
Dobšáková, Lenka ; Melichar, Jan (referee) ; Veselý, Jindřich (referee) ; Haluza, Miloslav (advisor)
This doctoral thesis studies the non-uniform blade cascade for centrifugal pumps. Influence of non-uniform blade cascade is investigated on the impeller and diffuser. A non-uniform blading impeller of pumps in this doctoral thesis was examined in terms of influence on efficiency characteristic. The idea of using non-uniform blading is to obtain a flat efficiency characteristic. Then the centrifugal pump could be used on larger scale of power with achieving a sufficiently high efficiency. The work is based on experimental measurements and numerical simulations of non-uniform hydraulic pump components. Non-uniform impeller and the diffuser were newly designed for this research. A new measuring track of small submersible pumps was needed to design and build for measurements. Different pump combinations with conventional hydraulics on one working point and hydraulics with non-uniform were measured. All measurements were evaluated and characteristics of efficiency, head and power were obtained for each measured combination. Some of pump combinations (which were measured in experiment) were numerically simulated by program Ansys Fluent. Data needed to evaluate the characteristic of efficiency and specific energy were collected from each numerical simulation. A theoretical consideration concerns the influence of non-uniform blade cascade applied on diffuser. The suggestion how to decrease hydraulic losses in canals was done. The theoretical consideration how to make a flat efficiency characteristic was made.
|
|
Vývoj metodologické a technologické platformy pro neinvazivní odhad fenolických látek v listech a bobulích
ŠEBELA, David
Plant optical signals can serve as important source of information about biochemical and physiological processes in plants. These signals are influenced by compounds synthesized by plants during primary or secondary metabolism and thus, can also serve as their qualitative and quantitative indicators. Light reaching plant surface (leaf or fruit) can undergo three main pathways- it can be (i) reflected, (ii) absorbed or it can (iii) transmit through plant material. The probability of these three processes depends on particular wavelength of incident irradiation and on the morphological characteristics of plant tissues themselves. As such, plant contains various spectrum of photosynthetic pigments and fluorescent compounds which can either reflect, absorb or pass incident irradiation through at specific wavelengths. Biophysical techniques working with these optical properties of plant pigments and/or other compounds have become universal and common tool in basic and applied research. To quote some example, chlorophyll fluorescence imaging, UV induced fluorescence or spectroscopic techniques are on the top of interest thanks to its non-invasive nature, allowing maintain the integrity of measured cells or the whole plant constituents. The main aim of this thesis is to provide a comprehensive study on the possibility of non-invasive monitoring of phenolic compounds in the leaves and fruits.
|
|
Marketing audit of the festival Divadelná Nitra
Surovková, Simona ; JEŽEK, Vlastimil (advisor) ; SYROVÝ, Daniel (referee)
Divadelná Nitra is an international theatre festival with over 20 years of tradition, which annually brings a selection of the best European productions of the season to Nitra. Visitors are offered a presentation of the top contemporary theatre productions, exceeding to dance, physical, visual and music theatre, new and inspirational art forms, rich accompanying and work programme, and many other art and cultural activities. The festival is an internationally recognized event and is of vital importance in the context of the current Slovak theatre. Yet, as many other non-profit organizations, it has been struggling each year to maintain a stable financial situation, and despite an enormous effort and an experienced management team, the festival cannot avoid some organizational problems. Several of them are related to marketing of the organization. The aim of this marketing audit is to analyze the current situation of the festival Divadelná Nitra, to evaluate the state of its own marketing activities, and, along with discovered results, to propose solutions that could help to improve marketing of the festival Divadelná Nitra.
|
|
The Importance of the Fundraiser in a Non-profit Organization
STARÁ, Radka
The main theme of the bachelor work is the importance of the fundraiser in a non-profit organization. It defines the term fundraising, its principles, forms and methods, the work of a fundraiser in a non-profit organization.The work characterizes nonprofit organizations, their legal status and field of activity. There are also information about activities, which improve economy and financial situation of these organizations. In the practical part of my work I have analyzed the way of financing a non-profit organization Junak- Czech scout, Centre Pod Kleti Holubov z.s. I am comparing in this part the way of fundraiser work on the local and state platform. The facts here available are drawn from the public web pages of this organization and also from the account keeping documents of its local center. At the conclusion of my work I am assessing the effectiveness of fund raising plan and its strategy and also describing the way of negotiation with donors. I am noticing the need of a fund raising team creation and also rules of fundraising including necessary cooperation between the center of organization and its local branches.
|
|
Monetary Policy and Macroprudential Policy: Rivals or Teammates?
Malovaná, Simona ; Frait, Jan
This paper sheds some light on situations in which monetary and macroprudential policies may interact (and potentially get into conflict) and contributes to the discussion about the coordination of those policies. Using data for the Czech Republic and five euro area countries we show that monetary tightening has a negative impact on the credit-to-GDP ratio and the non-risk-weighted bank capital ratio (i.e. a positive impact on bank leverage), while these effects have strengthened considerably since mid-2011. This supports the view that accommodative monetary policy contributes to a build-up of financial vulnerabilities, i.e. it boosts the credit cycle. On the other hand, the effect of the higher bank capital ratio is associated with some degree of uncertainty. For these and other reasons, coordination of the two policies is necessary to avoid an undesirable policy mix preventing effective achievement of the main objectives in the two policy areas.
Fulltext:  PDF
|
|
Dance as a means of integration adults with intellectual disability
KRAUMANNOVÁ, Eva
The goal of the bachelor thesis called Dance as a means of integration adults with intellectual disability was to create, implement and evaluate a dance course focused on the development of social competences in adults with intellectual disability. The thesis deals with adults with intellectual disability and with a leisure activity focused on dancing. There is some space for the development of social competences in adults´ leisure time. In response to the current situation of leisure activities proposition for adults with intellectual disability. I found it beneficial to found a dance group of adults with intellectual disability, and at the same time a group of individuals intact in places unfamiliar to them. Based on an activity which may be implemented amusingly it is possible to develop an individual´s personality as well as his or her social competences, which become a presumption of a successful integration, universally. The bachelor thesis consists of four chapters.The first chapter defines the term ´intellectual disability´. Further on the attention is paid to the characteristics of the target group, i.e. adults suffering from a slight and medium mental retardation. Further on, the disability´s impact onto the human psyche as well as social area is described. In the second chapter the term ´dance´is defined and then the description of its usefulness within the leisure, artistic and therapeutic areas is given. In the third chapter the presumptions for a successful integration are described. In the conclusion of the theoretical part there is an interconnection made between the target group and the activity for developing social competences. The theoretical part of the bachelor thesis is continued with a practical part, the fourth chapter. It is a programme of a six-month course which I have set together based on the analysis of expert literature and my experience gained during the leadership of dance lessons and working with adults with intellectual disability. The programme will include work methods and an evaluation of partial activities. The six-month course was held in the school year of 2015/2016 and 6 intellectually disabled adults took part in it. Students of the University of South Bohemia joined the course. Partial goals were set for individual dance lessons and the activities were set so that they would develop social competences in participants non-violently and in the greatest extent possible. The course was implemented in the IN Civic Association facilities. To evaluate the activity and find out the progress within the area of the participants´ social competences, several development fields have been set. Several chosen social competences were divided into evaluation scales. The participants were evaluated at the beginning of the course and then again, six months later. The evaluation method chosen was my own observation. I focused on the evaluation of my own working, on group evaluation and the evaluation of each individual. Evaluation was also done on the part of each course participant, too. Dance lessons and activities connected have proven to be a suitable means for developing social competences in intellectually disabled adults. In five participants the values have risen in 5 10 out of 17 competences observed. A recourse occured in a participant who was going through a difficult life situation during the last two months of the course. Values have risen dramatically and in all participants in the area of group cooperation. Five participants made a progress in establishing and keeping eye contact and in starting a conversation. One participant has made a progress in the area of group performance, another one has made a progress in the area of independence and another one started to call the other participants by their names, as opposed to the beginning of the course. In general, the members of the group became more self-confident.
|
guest ::
