|
Nájem bytu manželi a užívání družstevního bytu manželi v nové úpravě po 1.1.2014
Prantlová, Soňa ; Kadlecová, Eva (vedoucí práce) ; Pavla, Pavla (oponent)
Diplomová práce se věnovala tématu nájmu bytu manželi a jeho užívání tak, jak je to zakotveno v nové zákonné úpravě občanského zákoníku č. 89/2012 Sb. Ten nahradil do té doby fungující občanský zákoník z roku 1964. V nové právní úpravě je zakotvena řada nových institutů, jejichž cílem je především ochránit slabší stranu, v tomto případě nájemce. Diplomová práce byla rozčleněna na teoretickou a praktickou část. V teoretické části byla věnována pozornost základním pojmům, které zde byly definovány. Byla zde charakterizována práva nájemce a pronajímatele. Byla rozebrána právní úprava bydlení dle nového občanského zákoníku. Praktická část se věnovala interpretaci výsledků dotazníkového šetření. Byli osloveni nájemci několika bytových domů ve městě Kralupy nad Vltavou. Na základě dosažených zjištění byla navržena některá doporučení pro zvýšení informovanosti o právech a povinnostech nájemců, jakož i o celé problematice bydlení z právního hlediska.
|
|
Dílčí zpráva IV/2016 - Hodnocení monitoringu napěťodeformačního stavu horninového masivu při dobývání sloje 30 (634) v rámci zkušebního provozu dobývací metody chodba - pilíř v OPJ Dolu ČSM - SEVER
Waclawik, Petr ; Ptáček, Jiří ; Kukutsch, Radovan ; Kajzar, Vlastimil ; Koníček, Petr ; Souček, Kamil ; Staš, Lubomír
Monitoring napěťodeformačního stavu horninového masivu je nezbytným předpokladem pro ověření nové neschválené dobývací metody chodba-pilíř a jejího dalšího použití v podmínkách české části hornoslezské uhelné pánve. Tato dobývací metoda je projektována pouze na základě zkušeností a postupů, které jsou ověřeny v odlišných přírodních podmínkách a hloubkách pod povrchem a proto je nezbytná její verifikace pro podmínky české části hornoslezské pánve na základě geotechnického monitoringu. Předkládaná zpráva je zpracována na základě smlouvy o dílo č. 942/50/10, kde se Ústav Geoniky AV ČR, v.v zavazuje provádět pravidelné vyhodnocování dat monitoringu napěťodeformačního stavu horninového masivu. V souladu s výše uvedenou smlouvou, je zpráva zpracována v 6-ti měsíčním intervalu a navazuje tak na dílčí zprávu III/2015 (Waclawik et al. 2015) předanou odběrateli v dubnu tohoto roku. Průběžné výsledky geotechnického monitoringu, tak jak zkušenosti získané v době dobývání první dobývky V, ukazují na specifika přírodních podmínek v lokalitě zkušebního provozu nové neschválené dobývací metody chodba-pilíř.
Plný tet: UGN_0464907 -  PDF
Plný text: content.csg - PDF
|
|
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.
|
|
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.
|
|
Metodika aplikace testu obvodu založená na identifikaci testovatelných bloků
Herrman, Tomáš ; Plíva, Zdeněk (oponent) ; Racek, Stanislav (oponent) ; Kotásek, Zdeněk (vedoucí práce)
Dizertační práce se zabývá analýzou číslicových obvodů popsaných na úrovni meziregistrových přenosů. Je v ní zahrnuta pouze problematika související s testovatelností obvodových datových cest, řadičem ovládajícím tok dat těmito cestami se nezabývá. Stěžejní částí práce je návrh konceptu testovatelného bloku (TB), pomocí něhož se obvod rozdělí na části, jež jsou plně testovatelné přes jejich vstupy a výstupy, přes takzvané hraniční registry bloku nebo primární vstupy/výstupy. Přínosem nové metodiky je také redukce počtu registrů v řetězci scan, do něhož jsou zařazeny pouze hraniční registry. Segmentací obvodu dosáhneme také zjednodušení generování testu rozdělením tohoto problému na více menších částí. Navržená metodika pro identifikaci TB v číslicovém obvodu využívá dvou vybraných evolučních algoritmů operujících na formálním modelu obvodu na úrovni RT.
|
|
On-line Data Analysis Based on Visual Codebooks
Beran, Vítězslav ; Honec, Jozef (oponent) ; Sojka, Eduard (oponent) ; Zemčík, Pavel (vedoucí práce)
This work introduces the new adaptable method for on-line video searching in real-time based on visual codebook. The new method addresses the high computational efficiency and retrieval performance when used on on-line data. The method originates in procedures utilized by static visual codebook techniques. These standard procedures are modified to be able to adapt to changing data. The procedures, that improve the new method adaptability, are dynamic inverse document frequency, adaptable visual codebook and flowing inverted index. The developed adaptable method was evaluated and the presented results show how the adaptable method outperforms the static approaches when evaluating on the video searching tasks. The new adaptable method is based on introduced flowing window concept that defines the ways of selection of data, both for system adaptation and for processing. Together with the concept, the mathematical background is defined to find the best configuration when applying the concept to some new method. The practical application of the adaptable method is particularly in the video processing systems where significant changes of the data domain, unknown in advance, is expected. The method is applicable in embedded systems monitoring and analyzing the broadcasted TV on-line signals in real-time.
|
|
Synchronous Formal Systems Based on Grammars and Transducers
Horáček, Petr ; Janoušek, Jan (oponent) ; Yamamura,, Akihito (oponent) ; Meduna, Alexandr (vedoucí práce)
This doctoral thesis studies synchronous formal systems based on grammars and transducers, investigating both theoretical properties and practical application perspectives. It introduces new concepts and definitions building upon the well-known principles of regulated rewriting and synchronization. An alternate approach to synchronization of context-free grammars is proposed, based on linked rules. This principle is extended to regulated grammars such as scattered context grammars and matrix grammars. Moreover, based on a similar principle, a new type of transducer called the rule-restricted transducer is introduced as a system consisting of a finite automaton and context-free grammar. New theoretical results regarding the generative and accepting power are presented. The last part of the thesis studies linguistically-oriented application perspectives, focusing on natural language translation. The main advantages of the new models are discussed and compared, using select case studies from Czech, English, and Japanese to illustrate.
|
|
Extensions to Probabilistic Linear Discriminant Analysis for Speaker Recognition
Plchot, Oldřich ; Fousek, Petr (oponent) ; McCree,, Alan (oponent) ; Burget, Lukáš (vedoucí práce)
This thesis deals with probabilistic models for automatic speaker verification. In particular, the Probabilistic Linear Discriminant Analysis (PLDA) model, which models i--vector representation of speech utterances, is analyzed in detail. The thesis proposes extensions to the standard state-of-the-art PLDA model. The newly proposed Full Posterior Distribution PLDA models the uncertainty associated with the i--vector generation process. A new discriminative approach to training the speaker verification system based on the~PLDA model is also proposed. When comparing the original PLDA with the model extended by considering the i--vector uncertainty, results obtained with the extended model show up to 20% relative improvement on tests with short segments of speech. As the test segments get longer (more than one minute), the performance gain of the extended model is lower, but it is never worse than the baseline. Training data are, however, usually available in the form of segments which are sufficiently long and therefore, in such cases, there is no gain from using the extended model for training. Instead, the training can be performed with the original PLDA model and the extended model can be used if the task is to test on the short segments. The discriminative classifier is based on classifying pairs of i--vectors into two classes representing target and non-target trials. The functional form for obtaining the score for every i--vector pair is derived from the PLDA model and training is based on the logistic regression minimizing the cross-entropy error function between the correct labeling of all trials and the probabilistic labeling proposed by the system. The results obtained with discriminatively trained system are similar to those obtained with generative baseline, but the discriminative approach shows the ability to output better calibrated scores. This property leads to a better actual verification performance on an unseen evaluation set, which is an important feature for real use scenarios.
|
host ::
