Lazy Clause Generation (LCG) Solving is a state-of-the-art technique for solving finite domain problems. The combination of powerful Constraint Programming (CP) propagators and Conflict Driven Clause Learning (CDCL) from the SAT domain enables both powerful inferences and learning from conflicts. Most research has focused on strengthening propagator explanations but has limited itself to remain within the standard LCG protocol, which only uses basic assignment and bound literals.

This thesis will focus on structurally extending this CDCL resolution protocol with new literals. We investigate the addition of two different literals to this protocol: a partial sum inequality literal and a precedence literal specifically for the cumulative constraint.

We verify previous work on the inequality literal, expand the test suite, and take a dive into metrics specifically related to extended resolution. We propose the novel idea of the cumulative literal, assessing its performance. We evaluate these extensions against both a baseline solver without protocol extensions and against each other across a range of hyper-parameters and search strategies.

Our results show that extending the protocol is not a guarantee for performance, the linear inequality extension remains powerful in some scenarios but fails to improve on a series of benchmarks whilst the cumulative literal shows no improvement at all. Moreover, we find that structurally based extended resolution introduces overlap between the literals in a nogood which negatively affects nogood quality.

These findings showcase that the research is far from done. A powerful technique exists but future research should consider additional infrastructure to make sure these techniques flourish at their fullest potential.

Constraint Programming (CP) solvers are complex pieces of software with a large surface area for bugs, making it difficult to trust their claims of unsatisfiability or optimality. We make a contribution to the development of a CP unsatisfiability proof checker, which is formally verified in Rocq, by investigating how to develop checkers for individual proof steps. In particular, we develop formally verified checkers that can verify the reasoning performed by alldifferent and cumulative timetable propagators. We also introduce a methodology for supporting other propagators and constraints in the checker. We also contribute a formally verified integer domain representation using what we call perforated intervals. Perforated intervals are designed to efficiently interoperate with atomic constraints, which are at the heart of the CP proof system. They are an important building block for the verification of proof steps that combine previous proof steps to derive new facts, which we also part of our contribution, and are also used in our propagation checkers. Our results demonstrate the feasibility of a CP-native unsatisfiability proof checker and increase the understanding of propagation verification. Our work also provides important building blocks that can be used to support additional constraints and propagators.

The availability and reliability of online systems form the cornerstone of modern civilization. Companies actively try to minimize downtime during incidents, and publishing incident reports afterwards is a standard practice. However, what is missing is an overview of the distribution of the categories of causes leading up to the incident and their characteristics. This paper fills that research gap by answering the question of a relation between different categories of software changes causing the incidents, and their respective mean time to repair (MTTR). A taxonomy for classifying the root causes and time to detect (TTD) of incident reports was derived. A total of 258 publicly available incident reports authored by Google were scraped, and a zero-shot classification model was chosen to classify these. Additionally, the analysis focused on the time to repair (TTR) for each category. This found that incidents caused by software version incompatibilities have the highest MTTR of 69.8 hours, followed by code defects of 54.0 hours, while the other categories have values between 13 and 20 hours. Given that the TTR of an incident is primarily impacted by the number of skilled engineers available, having an estimate of the difficulty based on empirical data could help improve resource distribution based on early indications of root causes.

Modern businesses increasingly rely on software-driven operations, making system reliability a critical concern. Despite advances in automated operations, gaps remain in understanding how the primary causes of system failures manifest, impact operational severity, and evolve in cloud-native environments. This study analyzes 7,804 publicly available incident reports spanning 2014–2022 to examine trends in operational fault types across modern IT systems. A state-of-the-art large language model was employed to classify incidents into a consolidated fault taxonomy with an overall accuracy of 92 % and a macro-averaged F1-score of 0.89. The results reveal that Misconfigurations and Deployment Failures (32.3 %), External Dependency Failures (30.0 %), and Capacity Issues (16.1 %) are the most frequent fault types. Significant correlations were found between fault types and incident duration, with Security Incidents exhibiting particularly long resolution times. Temporal analysis shows a rising prevalence of Misconfigurations/Deployment Failures and Software Bugs, alongside a decline in Infrastructure Failures, reflecting the growing complexity and automation of modern IT environments. These findings contribute to a deeper understanding of evolving digital fragility, reveal how different fault types impact operational resilience, and offer actionable insights for improving incident management and system reliability.

This study examined common remediation strategies by analysing publicly available IT incident reports. A six-category taxonomy (“Software Fix”, “Rollback”, “Traffic Switch”, “Hardware/Infrastructure Repair or Operation”, “Self-Resolved”, and “Undisclosed/Not Specified”) was developed to classify implemented solutions. Subsequently, a corpus of 1268 recent public incident reports sourced from the VOID community database was collected, from which the solution description of each report is classified utilising a promptbased approach with the LLaMA3.3-70B-Versatile large language model (LLM). The LLM classifier
demonstrated substantial agreement (with Cohen’s κ = 71.4%, Macro F1 = 80.6%) with manual annotations on a ground truth subset of 127 reports. The primary findings revealed that a significant majority (76%) of the reports do not disclose specific technical solutions. Among reports with identifiable fixes, software fixes (5.5% of total) were the most common. Exploratory analysis also showed a statistically significant but small relationship between solution category and incident duration. This research highlights the utility of LLMs for analysing incident reports and powering AIOps and underscores the need for improvement in incident reporting.

Operational incidents in software-defined systems can lead to significant disruptions, and while primary faults such as bugs or misconfigurations are well studied, secondary issues that exacerbate these failures remain underexplored. This research investigates what secondary issues contribute to operational problems by analyzing 1,500 publicly available incident reports from platforms such as GitHub and the Verica Open Incident Database (VOID). Using a large language model (LLM) and a predefined classification schema, the study extracts and categorizes these issues at scale. The results show that communication failures (48.2%), monitoring and transparency deficiencies (46.5%), and documentation issues (41.1%) are the most prevalent secondary issues. These often co-occur, with the most common issue pair, communication failures and monitoring deficiencies, appearing together in over 600 reports, suggesting interdependent systemic weaknesses. Furthermore, these secondary issues show strong associations with different primary fault types, such as misconfigurations and software bugs, revealing distinct amplification patterns that affect incident severity and resolution time. A reproducible data pipeline was developed to enable large-scale analysis, and manual validation of model annotations yielded an accuracy of 81.9%, confirming the reliability of the LLM-based classification approach. The study addresses the feasibility of AI-assisted analysis for postmortem diagnostics and provides actionable insights into operational fragility, emphasizing the need to address not only technical faults but also organizational and process-level weaknesses.

Software changes are a leading cause of operational failures in complex production systems. Despite the increasing use of Artificial Intelligence for Development Operations and the availability of postmortem data, research on software incidents remains fragmented and narrowly scoped. This study aims to provide a generalizable understanding of software and change-induced incidents through structured analysis of 348 real-world incident reports from the Verica Open Incident Database. Using few-shot prompting with the GPT-4.1 Mini model, we extract key incident characteristics (root cause, triggering change, impact, severity, and remediation) and apply clustering to identify recurring incident archetypes. Our method achieves over 80% annotation accuracy on a manually labeled subset. We find that over half of incidents stem from software changes, with deployments and configuration updates disproportionately associated with high severity and manual remediation. Capacity issues and code defects are leading root causes. Clustering uncovers several prominent archetypes, including capacity-driven outages, defect-induced degradations, and hybrid failures involving improper changes. These findings support scalable incident analysis and can inform more context-aware operational strategies.

We consider a subset of simple proving exercises that are part of the Lean 4 tutorials. The exercises consist of a statement, and the task will consist of creating a proof term of the desired type through the use of tactics.
Large Language Models on their own are known to be able to produce syntactically correct pieces of text but are unable to come up with semantically correct pieces of text once very similar solutions are lacking in the dataset it was trained on.
This work reviews the Sequential Monte Carlo with Expectation-Maximization (SMX) algorithm for general reinforcement learning problems, and applies it to theorem proving using LLMs.
This work shows that the SMX algorithm is applicable to tasks where formal verification can be performed on the output, allowing the calculated reward to steer the reasoning process.
We furthermore formally prove a theorem that will be important in showing that the resampling step in SMX is necessary to mitigate sample impoverishment.
The theoretical part of this thesis builds on the theory of the SMX paper by verifying the derivation of the E-step, starting from the Evidence Lower Bound (ELBO). This derivation was missing from the original SMX paper.

Constraint programming is a paradigm used for solving complex combinatorial problems with applications in logistics, healthcare, telecommunications, and many other fields. Among the many constraints used in constraint programming is the inverse constraint, necessary for matching items one to one, such as the placement of containers on ships and task scheduling. This paper presents a novel propagator for the inverse constraint, leveraging the Dulmage-Mendelsohn decomposition, implemented in the Pumpkin solver, to improve the performance of the solver. Unlike decompositions of the constraint into other simpler constraints, our approach utilizes the full bipartite graph structure of the constraint, generating stronger and more reusable explanations for unsolvable states.
Experiments were conducted on benchmark problems taken from the MiniZinc challenge, including the Time-Dependent Traveling Salesman Problem (TDTSP) and Perfect One-Factorization (P1F). These experiments demonstrated the effectiveness of the propagator. Achieving up to a 35% reduction in the time taken by the solver for some instances of TDTSP,the method also highlights limitations in the symmetric application of the inverse constraint on a single array. These findings advance our understanding of the propagation of the inverse constraint and show the potential of graph based techniques to optimize LCG solvers. Future work aims to optimize the implementation and explore its performance in relation to a broader spectrum of techniques.

In this paper we embed a solution for bin packing problems in a constraint programming environment.
Existing solutions for bin packing problems are plentiful, but rigid.
We have taken existing solutions of bin packing in constraint programming, and analysed the steps this algorithm takes.
We then developed explanations for these steps in the form of boolean clauses.
Using these explanations, a constraint programming paradigm by the name of lazy clause generation is able to generate new rules, that prevent the solver from making the same mistake twice.
We have compared our implementation to two different solutions.
Firstly we compared it to a decomposition, where the bin packing constraint was broken down into many smaller and simpler constraints.
Secondly, we compared our implementation to a version with naive explanations.
In one benchmark, comparing our version to the decomposition in a pure bin packing problem, our implementation vastly outperformed the decomposition.
In other benchmarks, the results comparing our version to the other two were much more inconclusive.
While showing marginal improvements in some cases, our version performed worse in other cases.
The research performed in this paper definitely shows promise, and there is merit in exploring this approach in further research.

The regular constraint offers good balance between expressiveness and cost. Despite potential exponential blow-up, existing approaches use deterministic automata. Furthermore, the area of combining conflict-driven learning with regular is unexplored. We combine learning with non-determinism, to produce an NFA-based propagator with explanations, and compare its performance against decomposition of the constraint. Experimental results on Nonogram
instances indicate that our specialized propagator is significantly better than decomposing regular constraint.

In Constraint Programming, combinatorial problems such as those arising in the fields of artificial intelligence, scheduling, or circuit verification are modeled using mathematical constraints. Algorithms for each type of constraint are implemented in a solver and are known as propagators. Some constraints can be implemented using combinations of smaller existing propagators (this is known as decomposition), which is often used in Lazy Clause Generation (LCG) solvers, where research has shown that decompositions can be competitive or sometimes superior to purpose-built propagators for certain kinds of constraints. However, there is little research about whether a purpose-built propagator is superior to decomposition for the global cardinality constraint when used with an LCG solver. This paper benchmarks both approaches using an experimental Rust-based solver and uses existing algorithms to implement two global cardinality propagators which are then adapted for use in an LCG solver. The benchmarks show that both implementations are competitive or outperform decomposition in a dataset of 90 instances of Sudoku puzzles, being 3.19 and 2.28 times faster for Regin GAC and Basic Filter respectively. On the Minizinc Challenge dataset, the speedup factor is and 1.34 and 1.0.

The table constraint is a fundamental component of constraint programming (CP), used to explicitly define valid value combinations for variables. In modern Lazy Clause Generation (LCG) solvers, constraints rely on explanations to justify value removals and enable efficient conflict analysis through nogood generation. However, table constraints have primarily been implemented using direct SAT encodings, such as the state-of-the-art Bacchus method, rather than explanation-based approaches. This paper introduces two types of explanation-based propagators for table constraints: eager explanations, generated during propagation, and lazy explanations, which adapt explanations to specific conflicts for more general nogoods. Experiments on MiniZinc benchmarks show that Optimized (Lazy) explanations reduce conflicts by an average of 23% across all problems and up to 64% for specific instances compared to the Bacchus encoding, while also reducing learned clause length by 46%. Although the current implementations incur a runtime penalty of up to 2x, these findings highlight the potential of explanation-based propagators to improve conflict resolution and search efficiency with further optimizations.

The emergence of conversational AI systems like ChatGPT and Microsoft Copilot has impacted how users engage in information retrieval.
Retrieval Augmented Generation (RAG) harnesses the potential of Large Language Models (LLMs) with unstructured data, creating opportunities in science and business.
RAG-based models have gained popularity, but their effectiveness and user reliance in organizational settings call for exploration. This thesis involves a user study with policy experts in the financial domain.
They were tasked with text aggregation using a basic RAG model. The study delves into the model’s performance and the temporal development of user reliance among the experts over four weeks.
Our key findings reveal that outputs assisted by RAG do not match the quality produced by human experts.
The RAG model, however, excels in specific aspects such as structure, spelling, and grammar.
Additionally, the experts express satisfaction with the efficiency of RAG. Our findings suggest that user reliance on RAG increases with experience.
This underscores the need for interventions and policies to support responsible human-AI collaboration.
This work represents an effort to measure the temporal aspects of user reliance within an RAG system.
Simultaneously, it assesses the system’s efficacy in a field study with policy experts in the financial domain.

In recent years, GitHub Actions (GHA) has emerged as the leading platform for Continuous Integration and Continuous Deployment (CI/CD) within the GitHub ecosystem, offering developers seamless workflow automation. However, as with other CI/CD tools, GHA workflows are susceptible to ”smells” which are suboptimal practices that can lead to technical debt, reduced maintainability, and performance issues. This thesis investigates the prevalence and nature of these workflow smells in GHA configurations. Through an extensive analysis of commit histories from 83 projects, we identify common patterns of frequent changes in GHA workflows that may indicate the presence of smells. We propose a set of potential GHA-specific smells, develop a tool to automatically detect these smells, and validate our findings through a contribution study involving 40 pull requests to open-source projects. After qualitatively analysing the comments on 32 pull requests we settle on 7 confirmed GHA workflows smells, including one novel smell previously unrecognised in the literature, This work contributes to improving the quality of GHA workflows and offers insights for developers to optimise their CI/CD processes. Finally, this research was also accepted as a paper to the SCAM 2024 conference.

Reusable tools for engineering software languages can bridge the gap between formal specification and implementation, lowering the bar for engineers to design and implement programming languages. Among such tools belong NaBL2 and its successor Statix, which are meta-languages for declaratively specifying the static semantics of programming languages and generating typecheckers accordingly.

Although Statix intends to cover the domain of static semantics specification to a greater extent than NaBL2, less is known about how the meta-languages compare in terms of their practical usability.

In this thesis, we perform a case study in which we apply Statix to define the semantics of IceDust, an incremental computing DSL for modeling data with relations, and compare it to a prior NaBL2 specification.

We compare the novel and prior specification in order to determine how the meta-languages, when applied to the case of IceDust, compare in terms of high-level characteristics: expressiveness, readability, implementation effort and runtime performance. We perform four evaluations to this end: a qualitative in-depth comparison of the specifications, a measurement of specification sizes, an evaluation of correctness and a runtime performance benchmark of the resulting type checkers.

Our findings suggest that although Statix has a larger coverage of possible language definitions, in the case of IceDust it is a less expressive formalism for defining the static semantics and generates a slightly less performant type checker when compared to NaBL2. We find areas of interest for future work aiming to improve the practical usability of Statix, namely the definition of type compatibility relations, the way data in the scope graph are stored and retrieved and the integration with the compiler back-end.

Serverless computing is a relatively recent paradigm that promises fine-grained billing and ease-of-use by abstracting away cloud infrastructure for developers. There is an increasing interest in using the serverless paradigm to execute data analysis tasks. Serverless functions often interact with external services, which can be considered similar to the concept of side-effects in regular programming. Haskell uses monads to isolate side-effects and to structure the composition of functions using side-effects. This thesis explores whether the concept of the monad can be applied in a serverless computing environment, ideally in a way that is flexible with regards to platform. An abstraction of side-effects was developed in the form of a monadic layer that is added to serverless functions. The monadic layer interacts with monads using an interface and exposes the API of the monads to the user. A monadic implementation was also created for a platform-independent function composition mechanism using orchestrator functions. An implementation of a shared state side-effect has also been created as a practical use-case for the monadic layer, and to explore the usability of monads on platforms with more restricted composition frameworks. The implementations are evaluated on performance, expressiveness and usability.

Digital printing systems allow for the production of a large variety of different products. Making production plans for all these different products is challenging. One of the challenging aspects of making these production plans is choosing the right sequence of machines, to produce the desired intent. This is challenging due to three aspects: the large number of interdependent variables in the problem instances, the variability of machines, and the search for the best solution from a large set of valid solutions. In this thesis, we implement and evaluate the use of a domain-specific language (DSL) called RSX (Routing Space eXploration), to assist in choosing a sequence of machines. We do this together with an industrial partner. For RSX we use a model-driven approach, and it can be used to model the devices, production steps, and product properties of the digital printing domain. It transforms those into a constraint model described in the MiniZinc language, which is used as input for a constraint solver. We present the implementation of the RSX language and MiniZinc constraint model, and we evaluate the language coverage, accuracy, and performance. From these evaluations, we conclude that RSX can be used to model a number of cases, which were characteristic in the context of our industrial partner. Furthermore, we conclude that RSX can compile and solve the evaluated cases in the order of a few seconds and that the implementation is accurate, such that it can be used as a proof of concept.