In order to prevent, detect and fix errors in software, various tools for programmers are available, while some of them are able to reason about the behaviour of the program. In the case of C# programming language, the main representatives are Microsoft FxCop, Code Contracts and Pex. Those tools can, indeed, help to build a highly reliable software. However, when a company wants to include them in the software development process, there is a significant overhead involved. Therefore, we created a "light- weight" assertion verification tool called AskTheCode that can help the user to focus on a particular problem at a time that needs to be solved. Because of its goal-driven approach, we decided to implement it using backward symbolic execution. Although it can currently handle only basic C# statements and data types, the evaluation against the existing tools shows that it has the potential to eventually provide significant added value to the user once developed further. Powered by TCPDF (www.tcpdf.org)

Both J2BP and PANDA tools verify compiled Java programs. By now, these tools are not able to process some programs with specific JVM bytecode instruction sequences in the correct way. We described these instruction sequences and proposed their transformations. We developed the new application, called BytecodeTransformer, based on these propositions. This application transforms compiled Java programs and replaces the problematic instruction sequences with some others. Usage of BytecodeTransformer enlarges the set of programs that can be verified by both J2BP and PANDA. We also evaluated BytecodeTransformer on several Java programs, including own tests and well-known open-source programs. These tests demonstrated the correct functionality of BytecodeTransformer. Powered by TCPDF (www.tcpdf.org)

The thesis deals with design and implementation of controllers for the RMAP protocol, which is used by SpaceWire network endpoints to access memory contents of another endpoint. The theoretical research introduces concepts of the SpaceWire network, then describes the RMAP protocol and the AMBA AHB bus interface in detail. The practical part of this thesis then uses this information to design and implement controllers for the RMAP protocol. It first defines an architecture of these controllers, then describes design of individual blocks based on this architecture. As a next step, the thesis describes methods used to verify designed controllers and to test these controllers in an FPGA chip. Finally, an analysis of maximum frequency and usage of FPGA resources is done based on estimates provided by the synthesis tool.

The thesis is focused on the design and implementation of the portable stimulus verification scenarios for selected Berkelium processor modules based on RISC-V architecture from Codasip. The aim of this work is to use new standard for Portable Stimulus developed by Accellera organization to design and implement portable stimulus scenarios using the Questa InFact tool from Mentor. The proposed portable stimulus scenarios are then linked to the already existing verification environments of the UVM methodology and then they are used for verification of the Berkelium processor modules based on RISC-V architecture. The last part of the thesis is the evaluation of portability of the implemented scenarios to the individual levels of the Berkelium processor based on RISC-V architecture (IP blocks, subsystems, system level), in which it tries to use the proposed scenarios across all verificated levels.

The objective of this work is to study state-of-the-art deep neural networks based speaker verification systems called x-vectors on various conditions, such as wideband and narrowband data and to develop the system, which is robust to unseen language, specific noise or speech codec. This system takes variable length audio recording and maps it into fixed length embedding which is afterward used to represent the speaker. We compared our systems to BUT's submission to Speakers in the Wild Speaker Recognition Challenge (SITW) from 2016, which used previously popular statistical models - i-vectors. We observed, that when comparing single best systems, with recently published x-vectors we were able to obtain more than 4.38 times lower Equal Error Rate on SITW core-core condition compared to SITW submission from BUT. Moreover, we find that diarization substantially reduces error rate when there are multiple speakers for SITW core-multi condition but we could not see the same trend on NIST SRE 2018 VAST data.

Finite tree automata is formalism used in many different areas of computer science, among others in the area of formal verification. Nowdays there are few tools used for handling of finite tree automata, however libraries of MONA tool are the best choice. The finite tree automata are a frequent tool for formal verification of computer systems which work with dynamic data structures. The input format of finite tree automata for libraries of MONA tool is very difficult for humans because it is necessary to enter the move function of the finite tree automaton in a form of several multiterminal binary decision diagrams. The aim of this thesis is to design and implement tool to convert the finite set of move rules into internal format of the MONA tool.

This work deals with problems aging of unipolar transistors. In theoretical parts are described the mechanisms which causing aging unipolar transistors and way leading to the restriction the change of parameters in time. The measurement and data evaluation was built on theoretical knowledge. The model of aging FET is a result of this works; it is creating extraction of data from measured data. Finally, the degradation constants are evaluation from this data. This FET aging model is easy to use in simulators of electronics circuits including aging simulations (e.g. ELDO).

A brief introduction into biometrics is described in this thesis leading to description and to design a solution of verification system using speech analysis. The designed system provides firstly basic signal processing, then vowel recognition in fluent Czech speech. For each found vowel, observed speech features are calculated. The created GUI application was tested on created speaker database and its efficiency is approximately 54 % for short testing utterances, and approx. 88 % for long testing utterances respectively.

his thesis deals with the problems of cavitation flow in a Venturi tube. It is made for a multi-phase (water-vapour) flow calculation of two geometry tubes. Results of numerical calculations for the flow geometry (dimensions) are compared with performed experiment. Numerical flow calculation was performed in the Fluent 2.3.26.

In this work, we focus on improving the forest automata based shape analysis implemented in the Forester tool. This approach represents shapes of the heap using forest automata. Forest automata are based on tree automata and Forester currently has only a simple implementation of tree automata. Our first contribution is replacing this implementation by the general purpose tree automata library VATA, which contains the highly optimized implementations of automata operations. The version of Forester using the VATA library participated in the competition SV-COMP 2015. We further extended the forest automata based verification method with two new techniques - a counterexample analysis and predicate abstraction. The first one allows us to determine whether a found error is a real or spurious one. The results of the counterexample analysis is also used for creating new predicates which are used for the refinement of predicate abstraction. We show that both of these techniques contribute to an improvement over the early approach.