Defended dissertations

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.