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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

Programmers spend significantly more time trying to comprehend existing code than writing new code. They gain an understanding of the code by navigating the code base in an IDE, by reading documentation online, and by browsing code repositories on websites such as GitHub. To create rich experiences for programming languages across those various media is a large effort for developers of programming languages. This effort might be worthwhile for popular languages, but for new or experimental languages the required effort is often too large. Solutions to reduce this effort of implementing an IDE exist,such as LSP, but to reduce the effort in other places outside IDEs, we introduce the Codex metadata format, which separates language-specific generation of code metadata from its language-agnostic presentation. To demonstrate this approach by implementing four language-specific metadata generators (based on LSP, CTAGS, TextMate and Elaine) and two language-agnostic presentations (PDF documents and a code viewer websites) of code and metadata. To demonstrate different kinds of code metadata, we implemented four code exploration services: syntax colouring, code navigation, structure outline, and diagnostic messages. We show that with the Codex metadata format, we can decouple the metadata generators from the presentations.

Formal verification of imperative programs can be carried out on paper by annotating programs to obtain an outline of a proof in the style of Hoare. This process has been mechanized by the introduction of Separation Logic and computer assisted verification tools. However, the tools fail to achieve the readability and convenience of manual paper proof outlines. This is a pity, because getting ideas and proofs across is essential for scientific research. I introduce a mechanization for proof outlines of imperative programs to interactively write human readable outlines in the dependently typed programming language and proof assistant Agda. I achieve this by introducing practical syntax and proof automation to write concise proof outlines for a simple imperative programming language based on λ-calculus. The proposed solution results in proof outlines that combine the readability of paper proof outlines and the precision of mechanization.

The front-end of a compiler reads the source program and performs analyses such as type checking. The goal of the front-end is to check for the presence of syntactic and semantic errors before the program is passed to the back-end of the compiler for tasks such as optimization and code generation.

WebDSL is a domain-specific language for web programming that is being used for over 15 years. With WebDSL, many applications have been developed which have thousands of daily users. While the language has evolved over the years, the core of its implementation remains unchanged and is starting to show signs of a legacy system. The current WebDSL syntax is defined in SDF2 and all other parts of the compiler are implemented in Stratego.

This thesis presents a modernized front-end of the WebDSL compiler, utilizing the meta-languages of the Spoofax language workbench. Specifically, we introduce a syntax definition of WebDSL in SDF3 that is implemented without the use of post-parse filters, and an executable declarative specification of the WebDSL static semantics in Statix.

We use the modernized front-end as the largest case study to date for the meta-languages SDF3 and Statix, in order to evaluate their expressiveness, performance, and elegance when they are used to implement a real world language.

Nowadays does the internet presence of companies increase, and with it, their attack surface and the probability of breaches: every information system in the company's network may be an entry point for an outsider. Therefore, companies need to secure their information systems. However, current risk assessment frameworks fail to connect the security measures with the impact of future breaches, making it difficult for a company to prioritize their security investments: what security indicators should they look at to limit the impact of future intrusions? In this report, we study how to collect external security indicators from a company's network, and how to process this information to build an intrusion prediction model. First, we build a scanning tool to retrieve relevant security indicators from the company's network (such as services misconfigurations or vulnerabilities) and public datasets. Then, we associate the collected indicators with incidents data from a Managed Security Service Provider in order to model using a Random Forest algorithm the probability of intrusions. Finally, we analyze the most significant indicators according to the model in an effort to find which indicators are the most relevant to evaluate the company's security posture. When we assess our model on real company's data, it achieves 92% accuracy on intrusions prediction.

IoT devices keep entering our homes with the promise of delivering more services and enhancing user experience; however, these new devices also carry along an alarming number of vulnerabilities and security issues. In most cases, the users of these devices are completely unaware of the security risks that connecting these devices entail. Current tools do not provide users with essential security information such as whether a device is infected with malware. Traditional techniques to detect malware infections were not meant to be used by the end-user and current malware removal tools and security software cannot handle the heterogeneity of IoT devices. In this report, we design, develop and evaluate a tool, called NURSE, to fill this information gap, i.e., enabling end-users to detect IoT-malware infections in their home networks. NURSE follows a modular approach to analyze IoT traffic as captured by means of an ARP spoofing technique which does not require any network modification or specific hardware. Thus, NURSE provides zero-configuration IoT traffic analysis within everybody's reach. After testing NURSE in 83 different IoT network scenarios with a wide variety of IoT device types, results show that NURSE identifies malware-infected IoT devices with high-accuracy (86.7%) using device network behaviour and contacted destinations.

Static Analysis is of indispensable value for the robustness of software systems and the efficiency of developers. Moreover, many modern-day software systems are composed of interacting subsystems written in different programming languages. However, in most cases no static validation of these interactions is applied. In this thesis, we identify the Cross-Language Static Semantics Problem, which is defined as "How to provide a formal and executable specification of the static semantics of interactions between parts of a software system written in different languages?" We investigate current solutions to this problem, and propose criteria to which an all-encompassing solution to this problem must adhere. After that, we present a design pattern for the Statix meta-DSL for static semantics specification that allows to model loosely coupled, composable type system specifications. This pattern entails that the semantic concepts of a particular domain are encoded in an interface specification library, which is integrated in the type system of concrete languages. This allows controlled but automated composition of type systems. We show that, under some well-formedness criteria, the system provides correct results. A runtime, executing composed specifications, is implemented using PIE pipelines for partial incrementality, and integrated in the command-line interface and Eclipse IDE platforms, using the Spoofax 3 Framework. This allows using multi-language analysis in concrete projects. The design pattern, and the accompanying runtime are validated using two case studies. These case studies show that the approach is effective, even in a case where there is an impedance mismatch in the data models of the involved languages.

A recent advancement in Reinforcement Learning is the capability of modelling opponents. In this work, we are interested in going back to basics and testing this capability within the Iterated Prisoner's Dilemma, a simple method for modelling multi agent systems. Using the self modelling advantage actor critic model, we set up a single agent model that encodes its opponents, without requiring the opponents' actions directly. To verify that this technique is indeed capable of modelling opponents its capacity of encoding opponents is tested and the trained model is tested against several popular strategies. The embedding is found to not have a positive effect on the reward, only increasing the randomness of the model.