Serverless computing has transformed how distributed applications are built, enabling developers to deploy event-driven, scalable services without managing infrastructure. Early work on extending this paradigm to stateful applications through Stateful Function-as-a-Service (SFaaS) has shown that co-locating state with compute, effectively eliminating the "shipping data to code" problem, yields significant gains in throughput and latency. Systems such as Styx demonstrate that SFaaS can deliver serializable, exactly-once transactional guarantees across arbitrary function call-graphs at high performance. However, these performance benefits come at a cost: developers must decompose naturally sequential workflows into chains of asynchronous callbacks, manually managing continuations, context serialization, and distributed control flow, pulling attention away from business logic and toward distributed coordination.

In this thesis, we present Obol, a compiler-driven approach that raises the level of abstraction for SFaaS programming. Obol allows developers to express distributed stateful workflows as ordinary sequential, object-oriented code, and automatically compiles it to the asynchronous message-passing form required by the underlying runtime. We show that a multi-stage compiler pipeline can translate standard object-oriented constructs into correct distributed dataflow programs without sacrificing the transactional guarantees of the target runtime. We evaluate Obol on the YCSB and TPC-C benchmarks and demonstrate that the compiled code tracks hand-written operator latency to within a few percent up to saturation and saturates only modestly earlier. The residual gap is not compilation overhead, which a control workload isolates at essentially zero, but the cost of Obol's structured reply routing relative to hand-tuned callback wiring, a cost that the available concurrency constructs and optimizations significantly decrease. ... Read more

The integration of agentic artificial intelligence into software development workflows has introduced a new class of challenges for open-source software communities. As autonomous AI systems become capable of independently planning, implementing, and submitting code contributions, maintainers must deal with pull requests whose origin is not always disclosed and whose quality may not reflect sufficient human oversight. Despite growing community friction around this shift, evidenced by explicit AI contribution policies, controlled empirical studies of how maintainers actually respond to agentic AI contributions remain scarce.

This thesis investigates maintainer reception of agentic AI pull requests by actively submitting 90 pull requests to 45 open-source repositories across Python, TypeScript, and Java, targeting good first issues: tasks traditionally reserved for newcomers making their first contribution to a project. Contributions are structured along two dimensions: whether the repository has explicitly configured agentic AI tooling in its development workflow, and whether the use of AI assistance is disclosed in the pull request. This yields three contribution types, covering disclosed and undisclosed submissions to repositories without explicit AI configuration and disclosed submissions to repositories that have integrated agentic AI tooling. A mixed-methods approach is applied, combining quantitative analysis of acceptance rates and review activity with a qualitative thematic analysis of maintainer feedback.

The results show that acceptance rates differed across contribution types, with repositories that had explicitly integrated agentic AI tooling showing a statistically significantly lower acceptance rate compared to standard repositories with disclosed AI assistance, though not relative to the undisclosed group. Across all groups, staleness accounted for the majority of non-merged pull requests, suggesting that non-engagement was a more common outcome than active rejection. Disclosing AI assistance made no meaningful difference to acceptance rates within the same repository context. No statistically significant differences were found in the volume of reviews or comments across groups, although automated bots contributed a notable share of interactions, particularly in repositories with agentic tooling integration. Thematic analysis of maintainer feedback showed that code quality and implementation correctness were the dominant concerns across all groups, while explicit distrust of AI-generated contributions remained low. When maintainers did reject contributions on AI-related grounds, the concern was typically the degree of human oversight behind the submission rather than AI use itself. Several repositories also introduced or revised AI policies during the contribution period, reflecting how actively norms in this space are still evolving. ... Read more

Memory safety vulnerabilities present a critical challenge, driving both commercial and open-source projects to adopt the Rust programming language. Despite this trend, no previous research has examined the approaches taken by open-source projects migrating to Rust and their impact on software quality.

This thesis takes a mixed-methods approach to analyse the migration process. It introduces a novel, language-agnostic technique that helped identify 285 migrations by tracking Abstract Syntax Tree (AST) identifiers over time and across different repositories. Interviews with 38 of these projects revealed that they were migrating not only from C/C++ for memory safety, but also from higher-level languages such as Go, Python and JavaScript, in order to improve performance and maintainability.

Although project authors overwhelmingly report that their migration was successful, a quantitative analysis of the same projects across 22 metrics presents a more nuanced perspective. It shows testing practices improved post-migration, while some structural metrics showed a decline, with increased code duplication and significant reliance on `unsafe` code blocks. This highlights a possible discrepancy between developer perception and measurable code quality, suggesting that successful migration may be helped with more upfront architectural planning. ... Read more

Dependent type systems allow types to depend on values, enabling the encoding of rich semantic properties directly in types. Currently, dependently typed systems are not widely used for general-purpose programming, but they are commonly used in proof assistants. Agda, Idris, Lean, and Rocq all support dependent types.

The expressiveness of the type system comes with a cost: type checking is expensive. This thesis explores co-contextual type checking as an alternative foundation for dependent type systems. Co-contextual type checking inverts the ‘traditional’ flow of information, enabling type checking to proceed without immediate access to a complete typing environment.

This work explores a co-contextual formulation of a dependent type system and its accompanying type-checking algorithm. Both incremental and parallel variants of the algorithm are implemented for the dependently typed lambda calculus Elara, based on LambdaPi (Löh, McBride, and Swierstra, 2010). The research primarily focuses on the feasibility of such a type checker.

Apart from providing the first co-contextual implementation of a dependent type system, its performance is compared to LambdaPi’s contextual bidirectional type-checking algorithm for reference. In the end, it is found that the implemented co-contextual type checker generally performs worse than the contextual reference implementation. Its performance is of the same order of magnitude, with plenty of opportunity for improvement discussed in this work. In particular, co-contextual incremental type checking has significant potential through the reuse of evaluation, which is not fully leveraged in the conservative approach taken in this work. ... Read more

A key problem in program synthesis is that the search space is too big to traverse without a tactic. Budgeted search, specifically the Probe algorithm, is a promising one. Unfortunately Probe is treated as a monolith, instead of a collection of design choices. We identify these choices in the Herb-Probe algorithm and implement it in a budgeted search framework. Through its evaluation we learn more about Probe's design and create a framework for easy budgeted search comparison and hybridization. ... Read more

Program synthesis is the task of constructing a program that satisfies specified constraints. One popular formulation of program synthesis is example-based synthesis. Here, the synthesizer attempts to find a program in a specified domain that satisfies a set of input-output examples. Enumeration is the most common approach to finding the desired program. However, the exponentially growing search space makes this infeasible. The size of the domain can be largely attributed to its inefficient representation. Often, programs are only syntactically distinguished, meaning programs that behave the same are seen as different. We introduce Context-Sensitive E-Graph Saturation, a novel method that limits the search space to programs that solve at least one of the provided examples. This allows focusing only on programs that behave similarly to the desired one. Crucial is finding contextual equivalences for each example over a generated termset. These equivalences allow generating many solutions for each individual example. A program in the intersection of these programs solves all examples. In experiments on a subset from SyGus SLIA, our method solves the problems that enumeration solves, but not more. These results highlight a trade-off: with a small termset, the discovered equivalences are often too limited to capture the relationships needed to find a universal solution. Conversely, increasing the termset size quickly leads to inefficiency. To address this, we propose a strategy for constructing a more expressive yet small termset, enabling our method to solve a broader range of synthesis problems. ... Read more

A display map category, originally just called a class of display maps with a stability condition, can be used to model dependent type theory. There are several other constructions on categories that can serve a similar purpose, such as comprehension categories. In fact, the similarity of such concept has been well-known, and there even have been comparisons made using bicategories of such categorical notions.
In this thesis, I aim to formalise one such comparison, and implement it in a proof assistant. In order to do this, I needed to formalise display map categories, some related concepts, to then construct their bicategory, and show the comparison as a pseudofunctor into the bicategory of comprehension categories. The formalisation has been done using Univalent Foundations, while the implementation has been completed using Rocq, and more specifically the UniMath library.
... Read more

Code differencing allows understanding changes between different versions of software, especially when using Abstract Syntax Trees (ASTs) to structurally represent code. The Gumtree algorithm is the current state-of-the-art algorithm for AST differencing, however its main drawback is long runtimes, especially for large ASTs. The Simple and Hybrid variants aims to solve this issue with a heuristic-based recovery phase, but their evaluation has been limited to small ASTs. Benchmarks show that the Simple variant results in significant improvements in output quality and performance with very large ASTs, while the Hybrid variant has mixed results. Furthermore, increasing the max_size hyperparameter with the Hybrid variant has an unpredictable effect on output quality and a negative effect on performance, but min_priority can generally be set to 1. The Diff-Auto-Tuning optimization approach is deemed often unusable for large ASTs, though it can be used to find cases where the Hybrid variant outperforms the Simple variant on a single data point. ... Read more

Structural code differencing algorithms are used in software engineering tasks such as version control, code review, and change classification. While the Gumtree algorithm is a popular choice due to its performance and accuracy, it is inherently unstable: the output of a diff may change depending on the direction in which it is computed. A stable variant of Gumtree has been proposed to enforce directional symmetry in mappings. In this paper, we empirically evaluate the performance overhead of Gumtree Stable compared to the original Greedy variant. We also assess the impact of lazy evaluation, enabled by the HyperDiff framework, as a general optimization technique applicable to both variants. Our experiments on real-world code changes show that while stability introduces slight overhead in most cases, some cases see relatively large performance gains, averaging out to a runtime improvement when run on larger datasets. Additionally, lazy evaluation significantly reduces runtime for both Stable and Greedy variants. These findings clarify the trade-offs involved in adopting stable differencing and demonstrate how HyperDiff can be used to optimize structural diff computations independently of algorithmic stability. ... Read more

Traditional AST-based code differencing tools like ChangeDistiller struggle to scale on large codebases. HyperAST is a framework that models versioned code as a Directed Acyclic Graph (DAG) of Abstract Syntax Trees (ASTs), with deduplication of unchanged nodes and precomputed metadata. This approach has demonstrated effectiveness in improving the performance of the GumTree algorithm. However, its applicability to algorithms with fundamentally different matching strategies, like ChangeDistiller's bottom-up approach, was unclear. We ported ChangeDistiller to Rust and adapted it to leverage HyperAST's optimizations. Experiments on 1,046 real-world code change pairs from the Defects4J dataset demonstrate a 99.13% reduction in total runtime (~4.5 hours to 2.3 minutes) and a median per-file reduction of 98.97% (3149.25 to 31.55 milliseconds), all without altering the core algorithm’s behavior. Our research demonstrates that HyperAST's techniques can be applied beyond GumTree, significantly improving ChangeDistiller's runtime performance. ... Read more

As software evolves, understanding the differences between versions of code becomes more important. While text-based differencing is practical and widespread, it does not capture the structure of code. AST-based differencing solves this by using the structure of the code. Gumtree is a well known reference implementation of multiple structural diff heuristics. Gumtree Greedy is the original algorithm, while Gumtree Simple is a later version that was designed to scale better by making stronger assumptions.

In this paper, we compare ported versions of Gumtree Greedy, Gumtree Simple, and their lazified variants. They were implemented in the Rust-based HyperAST framework and tested on large-scale Java datasets. Our results show that Gumtree Simple uses significantly fewer CPU cycles compared to Gumtree Greedy. Due to suspected bugs in the implementation, we cannot yet conclusively measure the benefits of lazification. However, our implementation experience suggests that Gumtree Simple is easier to adapt and optimize for scalability. ... Read more

Version control systems rely on code differencing algorithms to track changes and support key development tasks such as merging, code search, and code reviews. Traditional differencing techniques operate on plain-text representations of source code, which sometimes fail to convey the original intent behind code modifications. To address this, modern algorithms operate on abstract syntax trees (ASTs), enabling more accurate and structurally meaningful edit scripts. However, computing differences between ASTs poses new challenges, especially in balancing edit script quality with runtime performance.

This paper investigates the evolution of AST differencing algorithms by analyzing a sequence of key refinements built on top of Xy - a foundational algorithm originally designed for XML. We evaluate three influential enhancements: GumTree’s optimal recovery strategy, the simplified recovery heuristic introduced in GumTree Simple, and HyperDiff’s use of a compressed AST representation. We evaluate each refinement independently using a shared benchmarking framework and a dataset of real-world Java code changes. Our results show how each refinement incrementally improves scalability, runtime stability, and script quality. These findings offer a deeper understanding of the design trade-offs in AST differencing and provide guidance for developing efficient and interpretable structural diff tools at scale. ... Read more

Graphs and richer property graphs are common models for real-world data. We typically run algorithms on such data to extract meaningful information. Using domainspecific programming languages (DSLs) is a common approach to expressing such algorithms, contrasting to general-purpose programming languages and declarative graph query languages. On one hand, algorithms in general-purpose languages are verbose and conceptually far removed from from the algorithm theory, as is the case for some community detection algorithms in DSLs. On the other hand, the DSLs that are available are insufficient to express all common graph analysis algorithms. The Green-Marl Intermediate Representation (GMIR) is such a graph algorithm DSL. As it has been built from the ground up, it only provides a minimal feature to support the algorithms it initially needed to support, similar to how other DSLs are developed. This specifically prevents frontier exploration algorithms and community detection algorithms to be expressed, such as Dijkstra’s shortest path and the Louvain clustering method. We use GMIR as a vehicle to introduce new domain-specific abstractions for algorithmic graph processing, targeting those algorithms. We evaluate our abstractions by implementing them in the commercial GMIR compiler, which we then use to compile various new algorithms to existing commercial graph processing platforms. This shows that we have successfully enabled more graph algorithms to be expressed in GMIR, even though there are still many algorithms that remain inexpressible. ... Read more

Wireless sensors are used in many critical application field such as agriculture, healthcare and transportation. Such sensors often use batteries, which have a limited lifespan and contribute to environmental damage in the form of waste. Batteryless sensors solve these problems, but come with their own challenges; they frequently experience power failures because their energy storage is limited. To make sure the system can make forward progress, Intermittent Computing (ImC) techniques are used to back up the system state before the power fails. One such technique consists of splitting the program up into tasks, and backing up the system state after a task has fully executed. Such a task-based approach requires a non-standard programming model, often with many keywords that need to be inserted manually. This increases the burden on the programmer, moving focus to inserting the right keyword at the right time and not forgetting anything, instead of focusing on the things that really matter. To solve this problem, this work Code Instrumentation for Task-based Intermittent computing Development (CITID), a compileand runtime ImC system that reduces the programmer effort of a state-of-the-art task-based ImC system by removing up to 96% of necessary manually placed keywords, while insignificantly affecting performance in most cases. ... Read more

Static type-checking allows us to detect ill-typed programs even before running them. However, the higher complexity of type systems may cause type-checker implementation to differ from their specifications. This causes bugs and makes it hard to reason about the type of systems. To close this gap between implementation and specification, a meta-language Statix was introduced. Using Statix, we can write a specification using constraints over scope graphs and terms. Successfully solving these constraints means that the program is well-typed. However, while Statix ensures that the implementation and specification correspond to each other, it does not offer a way for its users to formally reason about the type systems' specifications. To this end, we introduce a library called statix-in-agda. This library, written using the proof assistant Agda, includes the formalisation of scope graphs and embedding of Statix's constraints. We show how we can use our library to specify the type system of STLC-like language, prove that programs in this language are well-typed, and give type-preservation proof for a type system of a simple toy language with numbers and addition. ... Read more

The rise of graph processing has led to an increase in the usage of graph databases and the availability of various frameworks. Graph databases have become more accessible and, in specific instances, can compete with relational databases. Testing an application with a relational database backend has shown limited test coverage, and current test generators cannot cover every branch condition in graph processing applications. There is a lack of test methods specifically designed for applications that utilize graph structures.
This paper presents PGFuzz, a coverage-guided, schema-aware fuzzer for graph processing applications. PGFuzz utilizes existing graph generators to generate inputs and applies graph-specific mutations to alter the graph state. These mutations are schema-aware, designed to cover the graph model search space and satisfy logical conditions from real-world applications. The mutations involve adding new graph elements, removing graph elements, modifying existing elements, altering property values, and violating graph constraints. When compared against existing graph generators and a random byte mutation approach on the nine real-world examples in our benchmark suite, PGFuzz demonstrates an increase in coverage over time and detects more logic errors than the other methods. PGFuzz can cover all previously uncovered branching.
... Read more

Research on open-source software evolution gained popularity in the last decade focusing on the theoretical determining factors. Additional works studied growth patterns modeling using time series techniques on small projects and metrics samples or non-openly available larger datasets. Limitations in reproducibility and scalability of these methodologies add to the lack of research on time series methodologies applied to open-source software evolution. Thus, time series approaches from different domains are needed to address the multivariate nature of larger and variable samples of open-source projects and metrics time series data. This thesis aims to provide a reproducible and scalable framework to support researchers in studying open-source software evolution using patterns modeling, time series merging, multivariate time series clustering and multivariate time series forecasting. An openly available dataset of 1328 projects is built using relevant metrics extracted from a systematic literature review. The metrics time series are segmented and clustered to obtain generalized growth patterns: Steep; Shallow; Plateau. The sequence of patterns and their correlation are used to create three project clusters, from which prediction models for all metrics are trained to perform multivariate time series forecasting. Experiment results give confidence over the reproducibility and the scalability of the framework and show how the pattern shifts can be linked to real events in projects' histories. The thesis provides an additional perspective on open-source software evolution and can serve as a starting point for further studies. ... Read more

Static type systems can greatly enhance the quality of programs, but implementing a type checker for them is challenging and error-prone. The Statix meta-language (part of the Spoofax language workbench) aims to make this task easier by automatically deriving a type checker from a declarative specification of the type system. However, so far Statix has not been used to implement a type system with dependent types, an expressive class of type systems which require evaluation of terms during type checking.

In this thesis, we present a specification of a simple dependently typed language in Statix, and discuss how to extend it with several common features such as inductive data types, universes, and inference of implicit arguments. While we encountered some challenges in the implementation, our conclusion is that Statix is already usable as a tool for implementing dependent types. ... Read more

Technical debt is a term that describes the consequences of taking shortcuts or quick-and-dirty solutions in the software engineering process, in order to gain short term advantages in the development process of software projects. In this paper, we investigate the technical debt present at the fintech company Adyen, and the developers' experience with technical debt. We investigate their behavior towards testing and refactoring, and give insight into module health with the Delta Maintainability Model. With the conclusions from this research, we propose a novel gamification system called 'Code Karma' to address these technical debt issues, give insight into efforts that increase code quality and motivate developers to improve internal software quality. We found that the Delta Maintainability Model may be used to evaluate module health over time. Additionally, developers believe that 'Code Karma' has a positive influence on the internal quality of the system. ... Read more

There are an estimated 253 million blind and visually impaired people in the world. To grant them access to text publications that contain images, experts are employed to write image descriptions. There is both a societal and a legislative pressure to supply image descriptions to all new and archived publications within a number of years, yet the number of available experts is limited. The image description task for images in textual context is complex, since a fitting description combines salient elements from both the image as well as the context into a description, which also differs depending on the publisher and published medium.

Because of this complex nature, current automated systems are unable to reliably produce desirable results. Instead, this thesis focuses on developing software to assist the experts in their general image description task in order to improve their efficiency. Specifically, we use existing, commercially available automated tools to generate alternative representations of the data. To analyse the system, we develop a user interface to present all of the available data and design an experiment with a small group of experts to investigate the system's applicability and perceived usefulness. We find that such a system has great potential to assist the experts, but that it might be desirable to focus on a solution aimed towards a smaller subset of publications, so that domain-specific information sources can be exploited to improve the information quality. ... Read more