Formal verification methods offer a large potential to provide automated software correctness checking (based on sound mathematical roots), which is of vital importance. One such technique is abstract regular model checking, which encodes sets of reachable configurations and one-step transitions between them using finite automata and transducers, respectively. Though this method addresses problems that are undecidable in general, it facilitates termination in many practical cases, while also significantly reducing the state space explosion problem. This is achieved by accelerating the computation of reachability sets using incrementally refinable abstractions, while eliminating spurious counterexamples caused by overapproximation using a counterexample-guided abstraction refinement technique. The aim of this thesis is to create a well designed tool for abstract regular model checking, which has so far only been implemented in prototypes. The new tool will model systems using symbolic automata and transducers instead of their (less concise) classic alternatives.

Cílem konverze hlasu (voice conversion, VC) je převést hlas zdrojového řečníka na hlas cílového řečníka. Technika je populární je u vtipných internetových videí, ale má také řadu seriózních využití, jako je dabování audiovizuálního materiálu a anonymizace hlasu (například pro ochranu svědků). Vzhledem k tomu, že může sloužit pro spoofing systémů identifikace hlasu, je také důležitým nástrojem pro vývoj detektorů spoofingu a protiopatření.    Modely VC byly dříve trénovány převážně na paralelních (tj. dva řečníci čtou stejný text) a na vysoce kvalitních audio materiálech. Cílem této práce bylo prozkoumat vývoj VC na neparalelních datech a na signálech nízké kvality, zejména z veřejně dostupné databáze VoxCeleb. Práce vychází z moderní architektury AutoVC definované Qianem et al. Je založena na neurálních autoenkodérech, jejichž cílem je oddělit informace o obsahu a řečníkovi do samostatných nízkodimenzionýálních vektorových reprezentací (embeddingů). Cílová řeč se potom získá nahrazením embeddingu zdrojového řečníka embeddingem cílového řečníka. Qianova architektura byla vylepšena pro zpracování audio nízké kvality experimentováním s různými embeddingy řečníků (d-vektory vs. x-vektory), zavedením klasifikátoru řečníka z obsahových embeddingů v adversariálním schématu trénování neuronových sítí a laděním velikosti obsahového embeddingu tak, že jsme definovali informační bottle-neck v příslušné neuronové síti. Definovali jsme také další adversariální architekturu, která porovnává původní obsahové embeddingy s embeddingy získanými ze zkonvertované řeči. Výsledky experimentů prokazují, že neparalelní VC na nekvalitních datech je skutečně možná. Výsledná audia nebyla tak kvalitní případě hi fi vstupů, ale výsledky ověření řečníků po spoofingu výsledným systémem jasně ukázaly posun hlasových charakteristik směrem k cílovým řečníkům.

Contracts for concurrency describe required atomicity of method sequences in concurrent programs. This work proposes a dynamic analyzer to verify programs written in Java against contracts for concurrency. The analyzer was designed to detect violations of parametric contracts with spoilers. The proposed analyzer was implemented as an extension to the RoadRunner framework. Support for accessing the method arguments and return values was added to RoadRunner as a part of the solution. The analyzer was fully implemented and verified on a set of testing programs.

This diploma thesis deals with the identification of persons by their fingerprints. In the beginning, there is a brief overview of biometric methods. The issue of fingerprints and their automatic processing is very extensive and addresses a large amount of literature. This work describes the various stages processing fingerprints from receiving a fingerprint scan through the methods of enhancing fingerprint, binarization, the detection of minutiae to compare two fingerprints. After a short introduction of biometric techniques is briefly introduced the history of fingerprints as an instrument for identification of persons. Subsequently, there is the description of problems of obtaining fingerprints from older methods that require the transmission medium, to methods of obtaining fingerprints directly into a digital format. There are described basic principles of sensors and the principle of their function. Next part deals with methods of processing digital fingerprint images. These are methods for fingerprint image enhancement, methods for image thresholding, thinning of ridge lines, detection of global and local characteristics of the fingerprint. The next section introduces the basic methods of comparison and classification of fingerprints. The practical part describes the specific implementation of fingerprint processing chain. For each processing stage is implemented one selected method. The result is an application that allows displaying the output of each phase, the comparison of fingerprints 1:1 and also finds a fingerprint in the database, by comparing one fingerprint with many.

This master’s thesis deals with programming of control system for an automatic assembly line rear seats of passenger cars. The theoretical part describes assembly line, PLC, robot, electric nutrunner and intelligent camera Sick. Practical part of the thesis characterizes created programs of assembly workplace control system. This part also explains creating a model of station and subsequent formal verification of basic safety and functional properties.

This thesis is focused on proposal of production process of assembled crankshaft. It consists of choice of tools, data selection and optimisation for manufacture of individual components and for the assembly. In the assembly are also calculated important parameters for pressing components. Selected cutting conditions are experimentally verified.

First, a few bugs from a list of common bug were chosen and patterns describing these bugs were inferred. Then, detectors searching for such patterns were implemented as plug-ins to FindBugs static analyzer. Finally, detectors were used to detect bugs in development version of JBoss AS. Results are presented at the end of this paper.

This thesis deals with recognition by retina (identification, verification). In introduction we describe information about human eye, its diseases with focus on retina impact. Further (in main part) we conduct SW analyses based on biometry retina requirements and design of SW application for retina recognition. It is based on processing pipeline design (sequential application of image filters). This pipeline mostly contains filters focused on edge detection, adaptive threshold and skeletonisation. Finally, basic SW functions includes users registration (enroll), identification, verification. In conclusion we discuss experimental results and success of designed SW in practical application.

Tato práce se zabývá metodami pro behaviorální detekci malware, které využívají techniky formální analýzy a verifikace. Základem je odvozování stromových automatů z grafů závislostí systémových volání, které jsou získány pomocí statické analýzy LLVM IR. V rámci práce je implementován prototyp detektoru, který využívá překladačovou infrastrukturu LLVM. Pro experimentální ověření detektoru je použit překladač jazyka C/C++, který je schopen generovat mutace malware za pomoci obfuskujících transformací. Výsledky předběžných experimentů a případná budoucí rozšíření detektoru jsou diskutovány v závěru práce.

Tato práce se zabývá verifikací nekonečně stavových systémů, konkrétně, verifikací programů využívajích složité dynamicky propojované datové struktury. V minulosti se k řešení tohoto problému objevilo mnoho různých přístupů, avšak žádný z nich doposud nebyl natolik robustní, aby fungoval ve všech případech, se kterými se lze v praxi setkat. Ve snaze poskytnout vyšší úroveň automatizace a současně umožnit verifikaci programů se složitějšími datovými strukturami v této práci navrhujeme nový přístup, který je založen zejména na použití stromových automatů, ale je také částečně inspirován některými myšlenkami, které jsou převzaty z metod založených na separační logice. Mimo to také představujeme několik vylepšení v oblasti implementace operací nad stromovými automaty, které jsou klíčové pro praktickou využitelnost navrhované verifikační metody. Konkrétně uvádíme optimalizovaný algoritmus pro výpočet simulací pro přechodový systém s návěštími, pomocí kterého lze efektivněji počítat simulace pro stromové automaty. Dále uvádíme nový algoritmus pro testování inkluze stromových automatů společně s experimenty, které ukazují, že tento algoritmus překonává jiné existující přístupy.