Defended dissertations

In this thesis, we study classical graph problems through the lens of reconfiguration and game theory, offering alternative perspectives on well-known problems such as the Independent Set and Dominating Set.

In the first part, we focus on the reconfiguration frameworks known as Token Sliding and Token Jumping and provide novel results in this area. We present new polynomial algorithms for finding a shortest reconfiguration sequence under Token Sliding between dominating sets on trees and interval graphs. We also generalize the Token Jumping model to allow multiple tokens to jump within a bounded distance and characterize when reachability between two token configurations is guaranteed in this setting. Furthermore, we analyze the complexity of deciding reachability under the rule where each token may move at once to a neighboring vertex in one step.

We also consider the Multiagent Path Finding problem and its connection to reconfiguration problems. For Multiagent Path Finding, we provide new parameterized algorithms as well as improved hardness results. We demonstrate how both Multiagent Path Finding and generalizations of Token Jumping fit within a broader unified framework, allowing the application of results from generalized Token Jumping to variants of Multiagent Path Finding.

Finally, we contribute to the field of games on graphs. We prove that the game Romeo and Juliet, also known as the dynamic separator game, is EXPTIME-complete. Additionally, we study the m-eternal domination game, presenting efficient winning strategies for the attacker on trees.

Interval Constraint Satisfaction Problems (ICSPs) are fundamental for rigorous verification of safety-critical systems and validated computation, as they provide mathematically sound enclosures of variable domains in the presence of nonlinearities and numerical uncertainty. However, ICSP solving is computationally intensive and traditionally relies on CPU-centric solvers that are hard to scale toward modern massively parallel computing. This dissertation addresses the acceleration of ICSP solving by bridging interval methods with modern machine-learning (ML) computation stacks, with the goal of turning verified interval computation into a compiler-optimized, high-throughput workload.

Building upon a our original abstraction model, we decompose the solving pipeline into four levels: (L0) outward-rounded interval arithmetic, (L1) interval expression evaluation, (L2) contractor-based constraint propagation, and (L3) branch-and-prune search. The core contribution is an implementation and performance study of Levels 0-1 in TensorFlow, emphasizing computational graphs and XLA compilation. We realize IEEE-1788-style outward rounding within TensorFlow and evaluate three implementation strategies: a native two-tensor encoding, a structured composite design, and custom C++ kernels. To reflect solver behavior, we introduce a reproducible benchmarking methodology based on large generated expression graphs and quantify throughput and stability across execution modes.

The results confirm that graph-based execution and compilation are key enablers for high-throughput interval computation. Among the evaluated strategies, the native two-tensor encoding provides the strongest performanceengineering trade-off and can outperform established eager baselines by orders of magnitude on expression-graph workloads. Composite implementations are generally limited by tracing and object-level overhead, whereas custom C/C++ kernels provide an additional performance lever via fused, purpose-built operators at the cost of higher integration effort. The experimental evaluation is conducted on a widely available backend to ensure controlled, reproducible comparisons; importantly, the proposed design maps interval algorithms to tensor operations and compilation pathways that are inherently compatible with heterogeneous accelerators offered by machine-learning stacks.

Building on the validated L0-L1 foundation, we extend the architecture to the upper layers and propose a concrete, testable design for ML-backed propagation and search. The approach separates a flexible host-level control plane from a compiled, shape-stable data plane that processes fixed-size batches of boxes using masks, divergence-aware bucketing, and soundness guardrails. Derivative-heavy contractors are integrated via automatic differentiation as cached compiled graphs.

Finally, we outline a portability roadmap based on StableHLO with multi-backend execution (e.g., XLA and IREE). This positions verified interval computation on machine-learning infrastructure as a practical pathway toward next-generation parallel ICSP solvers.

The rapid growth of high-speed networks demands scalable and efficient processing architectures capable of operating at 100 Gbit/s and beyond. This dissertation thesis investigates FPGA-based network applications, with a focus on architectures that leverage external DRAM memories to overcome performance and scalability bottlenecks. The research is closely tied to practical network environments, where we partnered with the CESNET association, which is a Czech national education and research network operator, and were able to deploy on the backbone network CESNET2, providing real-world insights and data used in our studies.

The low evolvability of structured documents, such as data management plans (DMPs), limits their adaptability to changing requirements. This dissertation thesis addresses this challenge by applying Normalized Systems Theory (NST) and integrating machine-actionability to redesign document creation and maintenance. Following the Design Science methodology, we develop an evolvable transformation framework that ensures sustainable conversions between machine-readable and human-oriented formats, improving modularity and scalability. The research focuses on addressing evolving requirements, tailoring DMPs to diverse fields and organizations, enabling seamless migration between templates, automating assessments, and providing structured guidance for researchers. Our approach transforms traditional DMPs into machine-actionable formats, allowing automated evaluations using predefined metrics, reducing manual workload, and enhancing data management practices. The solution is rigorously evaluated and demonstrated through a prototype implementation and case study, showcasing its effectiveness in improving evolvability in data stewardship planning.

Client applications are central to modern software systems, acting as the primary interface between users and complex digital infrastructure. These applications not only shape the perceived quality of a system but also influence its usability, accessibility, and success. However, their development is hindered by rapid technological changes, fragmented ecosystems, and tightly coupled concerns across semantic structure, visual design, and platform implementation. This results in systems that are costly to maintain, hard to evolve, and prone to ripple effects when requirements change. Despite the rise of design systems and front-end frameworks, most contemporary development practices lack the formalism and modularity necessary for long-term sustainability. Existing modeling languages and architectures often fall short of supporting machine-actionable representations and reusable semantics. This creates a critical gap between theoretical modeling approaches and the production needs of client-side systems. To address this, we propose a novel approach that combines principles from Normalized Systems Theory (NST) with semantic technologies and formal modeling of user interfaces and design systems. This integration enables structured, evolvable representations and supports the automated generation of maintainable code. By applying NSTs design theorems and expander mechanisms to front-end systems-an area previously underexplored within NST-we aim to promote modularity and reduce ripple effects. Our research follows a design science methodology comprising five interlinked design cycles. These include a systematic review of UI modeling languages, the development of formal ontologies for UI and design semantics, a methodology for sustainable code architecture, and the implementation of model-to-code expanders. The approach was validated through real-world application scenarios and evolvability analyses. The contributions of this thesis demonstrate that it is feasible to construct sustainable and evolvable client applications by combining semantic modeling with NST principles. Our findings extend the applicability of NST to front-end software engineering and provide a foundation for future research into model-driven UI development, automated code generation, and cross-platform application design and development.

This dissertation thesis addresses the lack of explicit type information in Pharo (and similar dynamically typed ecosystems) that limits developer tooling such as navigation, completion, reverse engineering and classdiagram generation. The work proposes a unified way to gather and combine heterogeneous type hintsstatic analyses, runtime observations and lightweight namebased cuesbehind a single query interface with clear latencycoverage tradeoffs. The approach is implemented in an extensible combining framework with provenance, ranking and configurable policies (chaining and fusion), and is complemented by a data pipeline that mines largescale nametotype regularities from real code. The results are demonstrated in IDE prototypes (a type tree presenter, smarter sender/implementor lists and completion augmentation) and in an exploratory UML generator for batch use. Evaluation on representative Pharo packages focuses on fitness for purpose: how coverage improves under practical time budgets, how profiles make tradeoffs explicit, and where limits and threats to validity remain. The framework and mined priors are intended to be reusable by tool builders and portable to related dynamic environments.

Collective decision-making plays a vital role in multi-agent systems, political science, and economics. From voting systems and resource allocation to team formation, these problems share a common structure: a group of agents, each with individual preferences, must reach a joint decision. The field of (computational) social choice offers a rigorous mathematical framework for analyzing such processes and formalizing what constitutes a best outcome, while also investigating the computational challenges involved. Given the inherent complexity of aggregating diverse---and sometimes conflicting---preferences, it is no surprise that many of these problems are computationally intractable. Yet, because they arise in practical and socially significant contexts, finding viable solutions remains essential. Various approaches exist to address their complexity. This dissertation thesis builds on the observation that not all instances of hard problems are equally difficult. We adopt the lens of parameterized complexity, a framework that provides tools to identify (structural) restrictions under which efficient algorithms are possible. Our main contribution is a detailed parameterized analysis of five foundational problems in computational social choice. We begin with control by deleting projects in participatory budgeting---a generalization of multiwinner voting. Next, we investigate the fair assignment of delivery orders in the modern gig economy. Then, we study two classes of coalition formation games, each reflecting distinct facets of collective decision-making. Finally, we propose a computational model for assigning refugees to communities in a way that respects the preferences of both the newcomers and the inhabitants already living in the city.

Virtual reality is one of the fastest-growing fields in today's technology. The visual quality, the field of view, the time-warping, it all gets better and better every day. However, there is also one other important aspect of virtual reality that is not talked about that often, and yet it should – user interface. After several decades of being dependent only on a mouse and keyboard – devices which prevailed as controllers for personal computers – we finally can use other methods of input. To control the virtual environment, we can even use other parts of our body than hands – for example, utilize eyesight for eye-tracking or let our own feet carry us around the virtual world. This dissertation thesis deals with hand-tracking controllers for virtual reality. The goal is to create an intuitive controller with the use of optical sensors so the user does not have to hold or wear any device to interact with the virtual world. We proposed and implemented a set of algorithms to fuse the tracking data from multiple optical hand-tracking sensors that provide greater precision and tracking possibilities than a single optical sensor ever could. We tested our approach both in terms of precision and speed of algorithms and its usability in real-life scenarios. In all the tests, our approach outperformed the current state-of-the-art.

There is a lot of data everywhere, on the internet, in science, etc. But unannotated data themselves are of little value. The goal of this dissertation is to improve active deep learning for eicient and reliable annotation of large data sets, with a particular emphasis on astronomical spectra. To validate the suitability of active deep learning for large data sets of astronomical spectra, we applied an active deep learning method to discovery of rare astronomical objects. This method, which combines a convolutional neural network with active learning, successfully discovered a number of new objects, even though we did not have a large and representative training set. The success of active deep learning depends on predictive uncertainties, so we next explored methods for quantifying them. We developed two probabilistic methods: one for predicting spectroscopic redshift using the Monte Carlo dropout and the other for predicting the atmospheric properties of exoplanets using the deep ensemble method. However, predictive uncertainties must be reliable. Therefore, we have developed a method that facilitates the diagnosis of the causes of potential problems with these predictive uncertainties. This method uses an interpreter of a probabilistic integral transform histogram to facilitate this diagnosis. Overall, this dissertation advances the field of active deep learning and predictive uncertainties evaluation with potential applications beyond astronomy to any field with large data sets.

Recommender systems play a pivotal role in managing and personalizing vast amounts of data across domains such as e-commerce, entertainment, and social media. This thesis addresses two critical challenges in modern recommender systems: scalability in linear shallow autoencoders and the integration of semantic and interaction-based similarities using Transformer architectures. Building on the Embarrassingly Shallow Autoencoder (EASE), we introduce ELSA, a scalable linear shallow autoencoder designed to overcome the limitations of EASE on datasets with a large number of items. By leveraging a low-rank decomposition of the weight matrix and gradient descent-based optimization, ELSA demonstrates remarkable scalability and applicability to industrial-scale datasets. The second contribution extends ELSA to Transformer architectures, resulting in the development of beeFormer, a framework that effectively combines interaction data with semantic and vision representations. We demostrate, that training Transformers with interaction data can transfer knowledge between datasets while outperforming not only semantic similarity-based Transformers but also traditional collaborative filtering methods. Additionally, the thesis explores cross-domain recommendation, revealing the potential of Transformer models to transfer knowledge between domains like books, movies, and fashion. The use of Large Language Model (LLM)-generated descriptions is shown to improve cross-domain recommendations.

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.