Abstraction-Based Machine-Code Program Verification
Supervisor
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Reviewers
prof. Thomas Noll, Nian-Ze Lee, Ph.D., doc. RNDr. Pavel Parízek, Ph.D.
Summary
This dissertation thesis is focused on formal verification of machine-code systems using model checking with abstraction. The background and state of the art of machine-code model checking are presented, and weaknesses of previous approaches are noted. The author's research described in this dissertation thesis and previous conference proceedings articles presents novel solutions to the major problems of previous research: the systems are described in the Rust programming language and are inherently simulable, automatically converted to verification equivalents and verified within a novel framework based on Three-Valued Abstraction Refinement. Special care is taken to allow efficient verification of variables based on bit-vectors. The author has created a formal verification tool implementing the introduced techniques, and its performance is evaluated in the thesis. The tool can be used to verify arbitrary finite-state digital systems, with a special focus on systems with behaviour determined by machine-code programs. The created tool is free, open-source, and publicly available.
Synchronizing Finite String and Tree Automata and their Parallelization
Author
Ing. Štěpán Plachý
Supervisor
doc. Ing. Jan Janoušek, Ph.D.
Reviewers
Prof. Frank Drewes, PhD.,Prof. Dr. Andreas Maletti, RNDr. František Mráz, CSc.
Parameterized Algorithms for Hitting Subgraphs
Author
Ing. Radovan Červený
Supervisor
RNDr. Ondřej Suchý, Ph.D.
Reviewers
Prof. Dr. Henning Fernau, doc. RNDr. Jiří Fiala, Ph.D., Dr. Jesper Nederlof
Author
Ing. Jiří Nádvorník
Supervisor
prof. Ing. Pavel Tvrdík, CSc.
Reviewers
prof. Karine Zeitouni, Ph.D., Tim Jenness, Ph.D., Dr. Norbert Podhorszki
Author
Ing. Tomáš Kolárik
Supervisor
doc. Dipl.-Ing. Dr. techn. Stefan Ratschan
Reviewers
Prof. Dr. Martin Fränzle, Prof. Kazunori Ueda, Prof. Étienne André
Differential Power Analysis Countermeasures in Programmable Hardware
Author
Ing. Stanislav Jeřábek
Supervisor
doc. Ing. Jan Schmidt, Ph.D.
Reviewers
Dr. Vincent Grosso doc. Ing. Zdeněk Martinásek, Ph.D. Prof. Paris Kitsos, PhD.
Processing, checking, and modeling of textual requirements specifications
Supervisor
prof. Dr. Ing. Petr Kroha, CSc.
Reviewers
prof. Ing. Vojtěch Svátek, Dr. doc. Ing. Radek Burget, Ph.D. prof. dr. José Emilio Labra Gayo
Towards a Normalized Systems Gateway Ontology for Conceptual Models
Author
Ing. Marek Suchánek
Supervisor
doc. Ing. Robert Pergl, Ph.D. (FIT ČVUT) prof. Dr. Herwig Mannaert (University of Antwerp)
Reviewers
Univ. Prof. Henderik Alex Proper, Ph.D. assist. prof. Sérgio Guerreiro, Ph.D. prof. Markus Helfert, Ph.D.
Side-Channel Security of Embedded Devices
Supervisor
doc. Dr.-Ing. Martin Novotný
Reviewers
Mgr. Jakub Breier, Ph.D. assist. prof. Francesco Regazzoni assoc. prof. Ricardo Chaves
The Impact of Encrypted DNS on Network Security
Supervisor
prof. Ing. Hana Kubátová, CSc.
Reviewers
RNDr. Tomáš Jirsík, Ph.D. prof. Rémi Badonnel, Ph.D. prof. Ramin Sadre, Ph.D.
Ontologies in Recommender Systems
Author
Ing. Stanislav Kuznetsov
Supervisor
doc. Ing. Pavel Kordík, Ph.D.
Reviewers
prof. dr hab. inz. Krzysztof Goczyla Assoc. Prof. Aleksandra Klašnja Milicevic, Ph.D. Mgr. Ladislav Peška, Ph.D.
A string automata approach to tree pattern matching and indexing
Author
Ing. Eliška Šestáková
Supervisor
doc. Ing. Jan Janoušek, Ph.D.
Reviewers
prof. RNDr. Alexandr Meduna, CSc. prof. Philip Bille prof. Giovanni Pighizzini
Design of Systems Supporting Compliance Management
Author
Ing. Marek Skotnica
Supervisor
doc. Ing. Robert Pergl, Ph.D.
Reviewers
Ing. Petr Křemen, Ph.D. prof. Hans Mulder, Ph.D. Assist. Prof. Joao Luiz Rebelo Moreira, Ph.D.
Analyzing Large Code Repositories
Supervisor
doc. Ing. Jan Janoušek, Ph.D.
Reviewers
Prof. Tobias Wrigstad Max Schaefer, MSc., DPhil. Mgr. Tomáš Petříček, Ph.D.
Automatic Test Pattern Generation of Zero-Aliasing Test for General Output Response Compactor
Supervisor
doc. Ing. Petr Fišer, Ph.D.
Reviewers
Assoc. Prof. Paolo Bernardi, PhD. Dr. Stephan Eggersgluess Prof. Liviu-Cristian Miclea, PhD.
Similarity Search in Unstructured Data using Data-Transitive Models
Author
Ing. David Bernhauer
Supervisor
prof. RNDr. Tomáš Skopal, Ph.D.
Reviewers
doc. RNDr. Vlastislav Dohnal, Ph.D. Prof. Richard C. H. Connor, Ph.D. Assoc. Prof. Magnus Lie Hetland, Ph.D.
Linear Cryptanalysis of Baby Rijndael and Implementation Side Channels of AES
Supervisor
prof. Ing. Róbert Lórencz, CSc.
Reviewers
Assoc. Prof. Brice Colombier, Ph.D. Mgr. Jakub Breier, Ph.D. doc. Ing. Zdeněk Martinásek, Ph.D.
Randomized Indexing for Approximate Selection Queries on Multidimensional Arrays
Supervisor
prof. Ing. Jan Holub, Ph.D.
Reviewers
prof. Ing. Michal Krátký, Ph.D. Kwo-Sen Kuo, PhD. Dimitar Mišev, PhD.
Trust Management in Wireless Ad Hoc Networks
Author
Ing. Yelena Trofimova
Supervisor
prof. Ing. Pavel Tvrdík, CSc.
Reviewers
Prof. Dr. Stefan Schmid prof. Ing. Miroslav Vozňák, Ph.D. doc. Ing. Zdeněk Bečvář, Ph.D.
Knowledge Extraction from Multimedia Content
Supervisor
prof. Ing. RNDr. Martin Holeňa, CSc.
Reviewers
prof. Irina Perfiljeva, CSc., dr. h. c., prof. h. c. Assoc. prof. Neeta Nain, Ph.D. doc. Ing. Karel Zimmermann, Ph.D.
Complexity of Games on Graphs
Author
Ing. Václav Blažej
Supervisor
doc. RNDr. Tomáš Valla, Ph.D.
Reviewers
Prof., Dr. rer. nat. Robert Bredereck RNDr. Martin Balko, Ph.D. Paweł Rzążewski, PhD.
Predictor Factory: Learning from Relational Data
Supervisor
doc. Ing. Pavel Kordík, Ph.D.
Reviewers
Prof. Abdullah Uz Tansel doc. Mgr. Martin Nečaský, Ph.D. doc. Ing. Tomáš Kliegr, Ph.D.
Adapting Enterprise Engineering and Normalised Systems Theories to Develop a Methodical Framework Supporting Technology Transitions
Author
Mgr. Ondřej Dvořák
Supervisor
doc. Ing. Robert Pergl, Ph.D.
Reviewers
assist. prof. David Sardinha Andrade de Aveiro, PhD assist. prof. Sérgio Luís Proença Duarte Guerreiro, PhD. doc. Ing. František Huňka, CSc.
Testability and Physical Security: The Cell-Level Approach
Author
Ing. Jan Bělohoubek
Supervisor
doc. Ing. Petr Fišer, Ph.D.
Reviewers
Prof. Dr. Amir Moradi; Prof. Dr.-Ing. Miloš Krstić; prof. Michel Renovell, Ph.D
Low-Latency Optimizations and Architectures for Compression Algorithms implemented in (Programmable) Hardware
Supervisor
Dr. Ing. Sven Ubik
Reviewers
doc. Ing. Jan Kořenek, Ph.D.; doc. Ing. Jaroslav Zdrálek, Ph.D; Dr. Dirk Koch
Automatic Malware Detection
Author
Mgr. Martin Jureček
Supervisor
prof. Ing. Róbert Lórencz, CSc.
Reviewers
Prof. Mark Stamp; Assoc. Prof. Carles Mateu, PhD.; Ing. Sebastián García, Ph.D.
Hardware generated keys for cryptographic systems and protocols
Author
Ing. Simona Buchovecká
Supervisor
prof. Ing. Róbert Lórencz, CSc.
Reviewers
Assoc. Prof. Jens-Peter Kaps, PhD.; Assoc. Prof. Florent Bernard; doc. Ing. Dominik Macko, PhD.
The Ring Oscillator based PUF on FPGAs
Author
Ing. Filip Kodýtek
Supervisor
prof. Ing. Róbert Lórencz, CSc.
Reviewers
Prof. Kris Gaj, PhD.; Assoc. Prof. Brice Colombier; doc. Ing. Zdeněk Vašíček, Ph.D.
Advanced Methods for Asymmetric Heterogeneous Transfer Learning
Author
Ing. Magda Friedjungová
Supervisor
doc. RNDr. Ing. Marcel Jiřina, Ph.D.
Reviewers
Ing. Vojtěch Franc, Ph.D.; prof. Michał Choraś, Ph.D.; dr. inž. Mariusz Topolski
Comprehensibility in Network Intrusion Detection
Supervisor
prof. Ing. RNDr. Martin Holeňa, CSc.
Reviewers
doc. Ing. Tomáš Kliegr, Ph.D.; Ing. Martin Rehák, Ph.D.; Prof. Hisashi Kashima, PhD.
Side-Channel Analysis: Efficient Attacks and Fault-Tolerant Countermeasures
Author
Ing. Vojtěch Miškovský
Supervisor
prof. Ing. Hana Kubátová, CSc.
Reviewers
Dr. Paris Kitsos; Giorgio Di Natale, Ph.D.; Prof. Lejla Batina, PDEng.
Meta-optimizations for Cluster Analysis
Supervisor
doc. Ing. Pavel Kordík, Ph.D.
Reviewers
Assoc. Prof., Dr. rer. nat. habil. Arthur Zimek; doc. Ing. Jan Platoš, Ph.D.; doc. Mouzhi Ge, Ph.D.
Improvement of the Routing in Opportunistic Networks by the Application of Unsupervised and Supervised Machine Learning Techniques
Author
Ing. Ladislava Smítková Janků
Supervisor
doc. Ing. Kateřina Hyniová, CSc.
Reviewers
Eleonora Borgia, PhD.; Assoc. Prof. Dr. Floriano De Rango; doc. Ing. Ján Papaj, PhD.
Adaptive control algorithms of intelligent agents
Author
Ing. Martin Šlapák
Supervisor
Mgr. Roman Neruda, CSc.
Reviewers
doc. Ing. Jiří Vokřínek, Ph.D.; RNDr. Petra Vidnerová, Ph.D.; doc. RNDr. Gabriela Andrejková, CSc.
Reliable FPGA Architecture
Supervisor
doc. Ing. Jan Schmidt, Ph.D.
Reviewers
Assoc. Prof. Luca Sterpone, PhD.; Jorge L. Tonfat, PhD.; prof. Ing. Miloš Drutarovský, CSc.
(Nonlinear) Tree Pattern Indexing and Backward Matching
Author
Ing. Jan Trávníček
Supervisor
doc. Ing. Jan Janoušek, Ph.D.
Reviewers
Assoc. prof. Johanna Björklund, PhD.; prof. RNDr. Marie Demlová, CSc.; doc. Mgr. Adam Rogalewicz, Ph.D.
Time and Frequency Transfer in Local Networks
Supervisor
RNDr. Ing. Vladimír Smotlacha, Ph.D.
Reviewers
Assoc. Prof. Ant. Javier Díaz Alonso, PhD.; doc. Ing. Jaroslav Roztočil, CSc.; Ing. Tomáš Horváth, Ph.D.
Manipulating the Capacity of Recommendation Models in Recall-Coverage Optimization
Author
Ing. Tomáš Řehořek
Supervisor
doc. Ing. Pavel Kordík, Ph.D.
Reviewers
prof. RNDr. Peter Vojtáš, DrSc.; Prof. Dr. Martha Larson; doc. Ing. Michal Kompan, PhD.
Linked Data Based Knowledge Provisioning
Author
Ing. Milan Dojčinovski
Supervisor
doc. Ing. Tomáš Vitvar, Ph.D.
Reviewers
Prof. Dr. Harith Alani; prof. RNDr. Peter Vojtáš, DrSc.; prof. dr. ir. Ruben Verborgh
Dynamic Texture Modeling
Supervisor
prof. Ing. Michal Haindl, DrSc.
Reviewers
Assoc. prof. Renaud Péteri; doc. Ing. Jaroslav Křivánek, Ph.D.; prof. RNDr. Roman Ďurikovič, PhD.
Stream-wise Parallel Anomaly Detection in Computer Networks
Supervisor
prof. Ing. Hana Kubátová, CSc.
Reviewers
doc. Ing. Ondřej Ryšavý, Ph.D.; prof. Ing. Václav Přenosil, CSc.; Prof. Dr. Burkhard Stiller
Prediction and Analysis of Mission Critical Systems Dependability
Author
Ing. Martin Daňhel
Supervisor
prof. Ing. Hana Kubátová, CSc.
Reviewers
doc. Ing. Stanislav Racek, CSc.; Ing. Josef Strnadel, Ph.D.; Prof. Dr. Jaan Raik
Towards a decentralised peer-to-peer cluster
Author
Ing. Josef Gattermayer
Supervisor
prof. Ing. Pavel Tvrdík, CSc.
Reviewers
prof. Ing. Petr Tůma, Dr.; Prof. Dr. rer. nat. habil. Dr. h. c. Alexander Schill; dhr. prof. dr. Marian Bubak
Properties and Implementation Aspects of Residue Arithmetic for a Hardware Solver of Systems of Linear Equations
Supervisor
prof. Ing. Róbert Lórencz, CSc.
Reviewers
doc. Ing. Miloš Drutarovský, CSc.; doc. Ing. Zdeněk Vašíček, Ph.D.; Assoc. Prof. Kris Gaj, Ph.D.
Iris Analysis
Author
Ing. Mikuláš Krupička
Supervisor
prof. Ing. Michal Haindl, DrSc.
Reviewers
Assoc. prof. Maria De Marsico; doc. Ing. Radim Kolář, Ph.D.; RNDr. Jan Kalina, Ph.D.
On Indexes of Ordered Trees for Subtrees and Tree Patterns and Their Space Complexities
Author
Ing. Martin Poliak
Supervisor
doc. Ing. Jan Janoušek, Ph.D.
Reviewers
prof. Dr. František Franěk; prof. RNDr. Alexander Meduna, CSc.; prof. RNDr. Jaroslav Pokorný, CSc.
Texture modeling applied to medical images
Supervisor
prof. Ing. Michal Haindl, DrSc.
Reviewers
Ing. Milan Sonka, Ph.D.; prof. Dr. Ing. Jan Kybic; prof. Ing. Jiří Jan, CSc.
Dependable design methods for programmable circuits with respect to area overhead
Supervisor
prof. Ing. Hana Kubátová, CSc.
Reviewers
Ing. Josef Strnadel, Ph.D.; doc. Ing. Vlastimil Vavřička, CSc.; Assoc. Prof. Francesco Leporati, PhD.
Towards OntoUML for Software Engineering: Transformation of OntoUML into Relational Databases
Author
Ing. Zdeněk Rybola
Supervisor
doc. Ing. Karel Richta, CSc.
Reviewers
doc. RNDr. Petr Šaloun, Ph.D.; Ivan Luković, PhD.; Prof. Dr. Giancarlo Guizzardi
Adaptive Measurement of Material Appearance
Author
Ing. Radomír Vávra
Supervisor
prof. Ing. Michal Haindl, DrSc.
Reviewers
doc. Ing. Jaroslav Křivánek, Ph.D.; doc. Ing. Jiří Bittner, Ph.D.; Prof. dr. hab. Inz. Karol Myszkowski
Physical Fault Injection and Monitoring Methods for Programmable Devices
Supervisor
prof. Ing. Hana Kubátová, CSc.
Reviewers
Giorgio Di Natale, Ph.D.; Prof. Dr. Andreas Steininger; Ing. Jiří Kvasnička, Ph.D.
Generation of High-Speed Network Device from High-Level Description
Author
Ing. Pavel Benáček
Supervisor
prof. Ing. Hana Kubátová, CSc.
Reviewers
Prof. Giuseppe Bianchi; Ing. Katarína Jelemenská, PhD.; Assoc. prof. Dr. Alistair McEwan
Digital Circuits Testing Based on Pattern Overlapping and Broadcasting
Author
Ing. Martin Chloupek
Reviewers
doc. Ing. Richard Růžička, Ph.D.; Ing. Štefan Krištofík, PhD.; Prof. Dr.-Ing. Heinrich Theodor Vierhaus
Implicit Representations in Testing and Dependability of Digital Circuits
Author
Ing. Jiří Balcárek
Supervisor
doc. Ing. Jan Schmidt, Ph.D.
Reviewers
prof. Ing. Tomáš Hruška, CSc.; Prof. Raimund Ubar, PhD.; Prof. Matteo Sonza Reorda, PhD.
Rich Semantic Representations in Web Usage Mining
Author
Ing. Jaroslav Kuchař
Supervisor
doc. Ing. Tomáš Vitvar, Ph.D.
Reviewers
prof. RNDr. Peter Vojtáš, DrSc.; Dr. Roman Dumitru; Priv. Doz. Mag. Dr. Gerhard Wohlgenannt
Dependable Systems Design Methods for FPGAs
Author
Ing. Jaroslav Borecký
Supervisor
prof. Ing. Hana Kubátová, CSc.
Reviewers
Prof. Smail Niar, PhD.; Prof. Dr. Andreas Steininger; doc. Ing. Vlastimil Vavřička, CSc.
Hierarchical Dependability Models Based on Markov Chains
Author
Ing. Martin Kohlík
Supervisor
prof. Ing. Hana Kubátová, CSc.
Reviewers
Dr. Karl-Erwin Grosspietsch; doc. RNDr. Elena Gramatová, PhD.; doc. Ing. Stanislav Racek, CSc.
Algorithms and Data Structures for Very Large Sparse Matrices
Supervisor
prof. Ing. Pavel Tvrdík, CSc.
Reviewers
prof. Ing. Tomáš Kozubek, Ph.D.; doc. Ing. Jaroslav Kruis, Ph.D.; Salvatore Filippone, Ph.D.
Information Extraction and Data Acquisition for News Articles Filtering and Recommendation
Supervisor
prof. RNDr. Peter Vojtáš, DrSc.
Reviewers
Dr.-Ing. Sebastian Hellmann; RNDr. Radim Řehůřek, Ph.D.; doc. Ing. Jan Platoš, Ph.D.
Searching Regularities in Strings using Finite Automata
Reviewers
prof. RNDr. Alexander Meduna, CSc.; prof. RNDr. Marie Demlová, CSc.; Prof. William Smyth, Ph.D.
Natural Language Compression Using Byte Codes
Author
Ing. Petr Procházka
Supervisor
prof. Ing. Jan Holub, Ph.D.
Reviewers
Prof. Shmuel Tomi Klein; doc. RNDr. Tomáš Dvořák, CSc.; doc. Mgr. Jiří Dvorský, Ph.D.
Programmable and Customizable Hardware Accelerators for Self-adaptive Virtual Processors in FPGA
Author
Ing. Jaroslav Sýkora
Supervisor
Ing. Martin Daněk, Ph.D.
Reviewers
prof. Dr.-Ing. Christian Hochberger; prof. Dr. Chris Jesshope; prof. Ing. Róbert Lórencz, CSc.
Low-Latency Video Transmissions for Real-Time Collaboration with a Scalable Hardware Acceleration
Reviewers
doc. RNDr. Pavel Satrapa, Ph.D.; prof. dr. ir. Cees de Laat; Andre Georg Holzner, Ph.D.
Reliability Analysis of SRAM-based Field-Programmable Gate Arrays
Author
Ing. Jiří Kvasnička
Supervisor
prof. Ing. Hana Kubátová, CSc.
Reviewers
doc. Ing. Stanislav Racek, CSc.; doc. Michel Renovell, Ph.D.; prof. Ing. Viera Stopjaková, PhD.
Extendable and Scalable FPGA-based High-speed Packet Processing
Supervisor
prof. Ing. Hana Kubátová, CSc.
Reviewers
prof. Ing. Zdeněk Plíva, Ph.D.; Ing. Katarína Jelemenská, Ph.D.; Francesco Leporati, associate professor
Overlapping Non-dedicated Clusters Architecture
Supervisor
prof. Ing. Pavel Tvrdík, CSc.
Reviewers
doc. Ing. Jan Janeček, CSc.; RNDr. Filip Zavoral, Ph.D.; Prof. Dr. rer. nat. habil. Dr. hc Alexander Schill
Pattern Matching in Tree Structures
Reviewers
prof. RNDr. Alexander Meduna, CSc.; prof. RNDr. Jaroslav Pokorný, CSc.; prof. Bruce A. Watson
Market-based Resource Allocation in Non-Dedicated Clusters
Author
Ing. Michal Košťál
Supervisor
prof. Ing. Pavel Tvrdík, CSc.
Reviewers
prof. Ing. Jiří Šafařík, CSc.; doc. Ing. Pavel Čičák, Ph.D; dr. Srikumar Venugopal
Supporting Multiple Languages in Virtual Machines
Supervisor
doc. Ing. Vojtěch Merunka, Ph.D.
Reviewers
Prof. Stéphane Ducasse; doc. Ing. Vladimír Janoušek, Ph.D.; Dr. Alexandre Bergel