While cloud-native architectures promise massive scalability and decoupling, their reliance on managed distributed services introduces a hidden risk: vendor lock-in. Even services with similar functionality and identical APIs may differ in fundamental guarantees such as delivery, ordering, and consistency. These differences could lead to subtle, unpredictable errors during migration. Current infrastructure-as-code tools like Terraform focus on provisioning and fail to capture these underlying behavioural constraints.

To bridge this semantic gap, this thesis introduces a formal framework leveraging the Quint specification language to automate cloud service compatibility analysis. By representing distributed systems as rigorous compositions of partially ordered guarantees, this framework generates specific correctness invariants to verify compatibility between systems, defined in terms of invariant preservation across migrations. The approach is empirically validated through trace-based execution against a concrete Redis instance.

Our compatibility experiments reveal an asymmetry in cloud migrations: while key-value stores exhibit high interoperability (primarily bottlenecked by strict causality), message queue compatibility is highly fragmented by conflicting delivery (at_most_once) and ordering (fifo_ordering) invariants. Furthermore, we demonstrate an application of this framework by feeding these formal, invariant-based violations back into Large Language Models (LLMs) as structured guidance. Experimental results show this formal feedback drastically constrains the generative search space, reducing the median iterations required to synthesise a correct distributed system by approximately 58%.

Ultimately, this research provides a machine-checkable foundation to safely navigate cloud migrations, moving beyond ad-hoc testing to enable the verifiable design of genuinely cloud-agnostic architectures. ... Read more

The spread of climate change mis- and disinformation poses a big threat to society; addressing this is the goal of the Joint Interdisciplinary Project (JIP) 6.1.1, in collaboration with the National Police. This report details the development of the Climate Disinformation Tracker, an open-source proof-ofconcept tool designed to trace the earliest online occurrence of climate denial narratives on Platform X and provide insightful visualizations of related tweets. The methodology, adapted from the DisTrack architecture, utilizes KeyBERT for keyword extraction and a custom scraping pipeline relying on the Nitter front-end for data retrieval, followed by mDeBERTa-v3-base-mnli-xnli for natural language inference (NLI) to classify posts as entailing, neutral, or contradictory to a user-provided claim. Validation testing demonstrated that the tool correctly identified the source tweet in 72% of claims when incorporating the synonym component, thus validating the potential of this approach for misinformation
tracking. The primary constraints identified are the dependence on non-deterministic Nitter scraping, which introduces operational instability and a 500-character query limit, and the accuracy ceiling of the alignment model. Despite these limitations, the tool validates a functional approach for empowering the public and investigative journalists with traceable context. ... Read more

Automatic Speech Recognition (ASR) systems are becoming increasingly popular in this day and age. Unfortunately, due to inherent biases within these systems, performance disparities exist among specific demographic groups. Bias metrics can be used to measure this bias. Within ASR they represent a niche area that has not yet been thoroughly explored. The few bias metrics that exist in literature mainly centre around the performance differences between speaker groups. This paper proposes two new bias metrics that focus not only on performance differences, but also take the base performance into account: Weighted Performance Bias (WPB) and Intergroup Weighted Performance Bias (IWPB). Although the lack of ground truth makes the results less easily interpretable, the results show similar trends within the new metrics as those defined in literature: bias is greatest among non-native Dutch speech. ... Read more