Quantified formulas over linear integer arithmetic (LIA) are common in formal verification, yet they present significant challenges for satisfiability modulo theories (SMT) solvers such as Z3. In this paper, we explore whether quantifier elimination can improve solver performance on the 2-coin Frobenius Coin Problem, a benchmark involving quantified LIA formulas with structural simplicity. While Z3's default strategy relies on solving satisfiability of a quantified formula directly, we evaluate an alternative tactic-based approach using the \texttt{qe\_rec} tactic to eliminate quantifiers first and produce a quantifier-free formula, which is then solved by the general purpose SMT solver. We conduct benchmarking across 54 satisfiable instances involving pairs of prime coin denominations. Our results indicate that quantifier elimination achieves better performance in both runtime and memory usage, solving more instances and offering consistent speed-ups of up to 10$\times$ compared to the default strategy.

To solve floating-point SMT problems, a variety of algorithms can be used, but there is not one algorithm that truly stands out at solving any kind of problem, as most have their own specific subset of problems where they perform well. A solution to maintaining efficiency in solving any kind of floating-point SMT problem is to run many of these domain specific solvers in parallel, allowing the best to always come out on top. This paper aims to provide an insight into possible improvements using parallelization by running multiple solvers (in parallel) on a large and diverse set of problems. We show that by parallelizing diverse solvers we can obtain a significant speedup over individual solvers on complex problems.

Z3 is a widely used SMT solver with support for linear and non-linear arithmetic. While powerful, its performance is dependent on tactics -- user-defined strategies that guide the solving process. This paper systematically analyzes the performance of Z3 across various tactic sequences, including ones with parallelization, on benchmarks from SMT-LIB. The results reveal that certain problems can get a speed-up of up to 5 times with the appropriate strategy, however different approaches come with certain limitations. We explore a pattern in linear problems where parallelization and heavy preprocessing make a big difference to performance. Additionally, we discuss two non-linear benchmarks for which it is very evident that the right approach to tactic selection matters and there is no single optimal strategy in SMT solving. These are all important observations since SMT solvers are a key part of many industrial processes where speed and accuracy are crucial.

The Z3 SMT solver, a type of satisfiability solver used both in research and in industry, can give better performance by either improving the underlying
implementation or using domain-specific guidance. We present a way to simulate domain-specific help automatically by reducing the search space based on the model solution, and we use it to compare two implementations of Z3′s string solver – Z3str3 (weaker) and Z3-Noodler (stronger) – with and without domain-specific help. We find that Z3-Noodler sees significantly less improvement than Z3str3 because 1) the additional “helping” constraints are in fact occasionally counterproductive and 2) Z3-Noodler solves equivalent problems much faster than Z3str3, so the relative overhead of the additional constraints is more noticed.

Satisfiability modulo theories solvers serve as the backbone of software verifiers, static analyzers, and proof assistants; the versatile bit-vector arithmetic theory is particularly important for these applications. As solvers continue to be developed, they become more capable but also more difficult to configure optimally. The widely-used Z3 prover offers a multitude of configurable techniques for solving bit-vector problems, however, the pace of development has not allowed for a comprehensive comparative analysis of them. We study the available bit-vector algorithms and parallelization methods, on established sets of problems. Through an experimental evaluation, we find that properly configuring Z3 for a specific use case can have significant effects on performance. We offer guidance to developers on how to go about that, which should help to make formal verification tools more efficient.

Alzheimer’s disease (AD) is a neurodegenerative disease affecting roughly 40 million people. 70% of the heritability of AD is expected to be explained by Structural Variants (SVs), however these have been scarcely studied in the context of AD. This study aims to find SVs associated with AD and to investigate the properties of these correlated SVs. To this end, a dataset created using Third Generation Sequencing of Single Nucleotide Polymorphisms (SNPs) and their correlation with SVs was utilised and combined with the full summary statistics and fine-mapped results of a large AD Genome Wide Association Study. This resulted in 85 unique SVs with significant correlations to known AD associated SNPs, of which 5 were also discovered in previous research, and 80 were novel. SVs were then associated with their nearest genes, however this resulted in a relatively low overlap with known AD genes and few to no results when applied to Gene Set Enrichment Analysis. Additionally, the data was tested for enrichment of Tandem Repeats (TRs), Transposable Elements, regulatory elements and mechanisms of gene expression, which found enrichment of TRs and heterochromatin areas and a depletion of deletions, weak enhancers, and transcription elongation areas.

Coronary artery disease (CAD) is a condition characterized by the narrowing or blockage of the arteries that supply blood to the heart. It is a major global health burden and is known to be correlated with genetics, but the details of the genetic contribution remain unclear. In this study, we explored the associations between structural variants (SVs) and single nucleotide polymorphisms (SNPs) identified through previous CAD genome-wide association studies (GWAS). We identified the most relevant associations by ranking them using a proposed composite score, combining effect sizes and p-values. Filtering was applied to keep the most significant associations within a 500kb genomic window, resulting in 968 SNP-SV associations. Cross-referencing with tissue-specific eQTL data from the GTEx Portal indicated 321 SNP-SV associations that impact gene expression in coronary artery tissue. GSEA identified associated pathways involving dopachrome isomerase, phenylpyruvate tautomerase, and
catalytic activity. The results suggest that the SVs make an important contribution to the regulation of CAD-related gene expression and the overall risk of CAD.

Genome-wide association studies (GWAS) are commonly used to identify genetic variants associated with human traits by comparing genetic differences between diseased and healthy individuals. One way to gain insights into the biological consequences of these variants is to use quantitative trait locus (QTL) analysis. These connect SNP with variations in gene expression levels among individuals. QTL studies are mostly done on single nucleotide changes, but as SVs are bigger and have greater impact on traits, SV-QTL connections are of great interest. Using Gosling.js, a tool was developed to easily display the links and significance between SNPs, associated eQTLs, and SVs. The main purpose of this tool is to provide clear visualizations, while also offering options for further exploration of the chromosome. The existing search functionalities from snpXplorer have been integrated and enhanced. Users can define a variable window size before querying, allowing for flexible data examination. Additionally, the tool supports requests for data across multiple tissues. For improved performance and usability, the option to select which data tracks are shown were added.

in bio-informatics visualisations are often used to relay the results of genome-wide association studies (GWAS), which can be used to get a better inside into the genetics of diseases. Over the years many websites have been developed, which can create visualisations for a variety of GWAS, with one of the most famous being locuszoom. Recent advancements in technology have allowed for collection of data which wasn't previously possible and which no visualisation tool currently supports. For the first time it is now possible to collect data on the interactions between two different types of genetic mutations: Single Nucleotide Polymorphisms, which consist of a single change in one nucleotide (one letter in a string of DNA) and Structural Variants, which consist of a change in a series of nucleotides. This paper builds upon an already existing visualisation tool snpxplorer and the goal is to design a visualisation, which captures thesse interactions and to add a new, easily integratable section to snpxplorer containing this new visualisation.

Effective onboarding in software engineering is critical yet challenging due to the rapid evolution of technologies, languages, frameworks, and tools. Traditional exploration, documentation and workshop-based onboarding methods tend to be expensive, time-consuming and can get outdated very fast in large, complex projects.

In this thesis, we introduce a novel solution: the Onboarding Buddy system which uses large language models (LLMs) and retrieval augmented generation (RAG), enhanced by an automated approach for chain-of-thought (CoT) that improves onboarding for new and existing developers. It integrates natural language explanations available in the development environment with relevant information, code explanations, and project-specific guidance. The system architecture is agent-centric, including contextualization, onboarding agents, instruction step processors and message enhancement agents that cooperate in delivering comprehensive, customized support with minimal reliance on human mentors.

While effective in supporting the completion of tasks and reducing stress related to onboarding, feedback also revealed some areas for improvement, like better context awareness, explicit instructions, improved technical stability, and UX adjustments. In general, Onboarding Buddy is an excellent promise to smoothen the onboarding process and therefore increase developer productivity and job satisfaction.

The experimental results demonstrated the system's effectiveness: participants spent an average of 175 minutes actively engaged in the IDE, completed tasks with nearly 100\% accuracy, and gave high helpfulness ratings (3 out of 4). Task completion times averaged 50 minutes, with simpler tasks taking around 28 minutes and complex ones requiring 67 minutes. User feedback showed high satisfaction (3.35/4 for understanding, 3.15/4 for accuracy) and strong interest in such solutions (7.75/10). Interestingly, more experienced developers spent more time on tasks, suggesting a deeper exploration of the codebase. A strong positive correlation (0.70) between system usage frequency and perceived helpfulness indicated that increased engagement led to better outcomes.

In other words, while there are areas for improvement, such as context awareness and processing complex tasks, this research proves that LLM-based onboarding solutions are feasible and can have significant positive impacts on the software engineering onboarding process, thus laying the foundation for future progress in automated developer support and knowledge sharing for software development.

The rapid advancement of Quantum Network architectures necessitates a comprehensive and quantitative comparison to assess their effectiveness and performance. Unfortunately, there does not exist an implemented quantum network benchmark suite capable of determining the superior architecture. Hence, our study aims to establish the foundation for developing a benchmark suite by leveraging existing quantum network applications. However, the specific inclusion of quantum network applications in the suite remains to be determined. Therefore, to address this gap, our study will explore the potential inclusion of the Clauser-Horne-Shimony-Holt (CHSH) game based on its effectiveness in identifying errors within various properties of the quantum networking system. We use an exploratory research methodology involving experiments performed on simulated quantum networks utilizing SquidASM. Each experiment simulates multiple quantum networks, with a single property as the independent variable. For each value of the independent variable, we calculate both the success probability of the game and the number of successes per second. Subsequently, we employ the one-way ANOVA test to examine if there are significant variations in these performance metrics. Our results demonstrate that the CHSH game exhibits sensitivity to all properties affecting the quality of entanglement between nodes, execution time, and the error probability of both single-qubit gates and measure operations. Additionally, we compare the success probabilities based on different input combinations using the Root Mean Squared metric to uncover any underlying patterns within the data. As a result, we discovered a procedure for quantifying the difference between the error probabilities of measurements of zero and one. Based on the outcomes of our study, we consider the CHSH game to be a suitable addition to the benchmark suite if the testing requirements of the suite align with the qualities offered by the application. We anticipate that these results will aid the development of the benchmark suite and advance the understanding of quantum network architectures and their evaluation

In the development of any new technology, it is essential to have methods to assess the quality of a system, to compare different systems to one another, and to compare different versions of the same system, to see if changes to the system can actually be classified as improvements. For quantum networks, this is no different. To further develop quantum networks, we need a benchmarking suite to judge the quality of such systems.

The aim of this research is to determine the effectiveness of blind quantum computation - a quantum network algorithm - as a benchmark. We determine what changes to the system affect the results of executing this application, and we use this to determine whether it would be effective to use this application as part of a larger benchmarking suite. We do this by simulating a quantum network, and manually varying system parameters one by one, to see if they have an effect on the results.

What we observed from these experiments is that blind quantum computation is sensitive to almost all system parameters. This means that introducing an imperfection into almost any system parameter will negatively affect the results of the application. This means the application is useful as a full-system benchmark, because it is affected by almost the entire system. However, it also means that the application is less useful as a benchmark for individual parameters.

This means that to make the most useful benchmarking suite, blind quantum computation would have to be combined with other quantum network applications that are more suitable for benchmarking individual system parameters.

Quantum networks provide numerous potential benefits over classical networks, such as enhanced security and faster computation, making their further development a lucrative prospect. As is the case with any technology, the advancement of quantum networks relies on the development of frameworks to test their quality, and compare different implementations of the technology. One such framework is a benchmarking suite for quantum network systems, that can identify areas for improvement in their implementation, by determining the erroneous properties of the system.
This paper examines the viability of using a specific quantum network application as a benchmark for quantum network systems. In order to quantify the application's ability to benchmark, we assess its sensitivity to changes in the properties of the system. These properties include link parameters, quantum gate properties, qubit coherence times, and measurement properties.
We use the BB84 protocol as the benchmarking application for this project, which is a Quantum Key Distribution scheme used to establish secure keys between two parties. In particular, we use the qubit error rate and the key generation rate as the performance metrics for the application. For the setup of the experiments, we prepare two system configurations: generic quantum device nodes with a depolarising error channel, and NV device nodes with a heralded link. In order to assess how the application behaves with changes to different system properties, we observe how the performance metrics change while individually varying system parameters and keeping all other parameters constant.
We find that the application is sensitive to changes in multiple parameters across both network configurations, such as link parameters, single qubit gate properties, and measurement properties. Contrarily, the application is not affected by changes to parameters such as two qubit gate properties and coherence times. We conclude that the BB84 protocol can be used as an individual localised test for the parameters it is sensitive to, and also in combination with other applications, in a more comprehensive benchmarking suite, that provide coverage for a broader range of parameters.

Writing unit tests is a crucial task in the software development lifecycle, ensuring the correctness of the software developed. Due to its time-consuming and laborious nature, it is, however, often neglected by software engineers. Numerous automatic test generation tools have been devised to ease unit testing efforts, but these test generation tools produce tests that are typically difficult to understand. Recently, Large Language Models (LLMs) have shown promising results in generating unit tests and in supporting other software engineering tasks. LLMs are capable of producing natural-looking (human-like) source code and text. In this thesis, we investigate the usability of tests generated by GitHub Copilot, a proprietary closed-source code generation tool that uses a LLM for its generations and integrates into well-known IDEs. We evaluate GitHub Copilot’s test generation abilities both within and without an existing test suite. Furthermore, we also evaluate the impact of different code commenting strategies on test generations, both within and without an existing test suite. We devise aspects of usability to investigate GitHub Copilot’s test generations. In total, we investigate the usability of 290 tests generated by GitHub Copilot. Our findings reveal that within an existing test suite, approximately 45.28% of the tests generated by Copilot are passing tests. The majority (54.72%) of generated tests in an existing test suite are failing, broken, or empty tests. Furthermore, tests generated by Copilot without an existing test suite are less usable compared to those generated within an existing test suite. The vast majority (92.45%) of these test generations are failing, broken, or empty tests. Only 7.55% of tests generated without an existing test suite were passing, and most of them provided less branch coverage when compared to human-written tests. Finally, we find that tests using a code usage example comment resulted in the most usable generations within an existing test suite. In contrast, when there is no existing test suite, a comment combining instructive natural language combined with a code usage example yielded the most usable test generations.

Background: For rigorous software testing, integration and end-to-end tests are essential to ensure the expected behavior of multiple interacting components of the system. When software is subjected to integration or end-to-end tests, it is often unfeasible to test every code change individually, as the runtime of these tests is usually significantly larger compared to unit tests. For this reason, batches of code changes from multiple authors are often tested simultaneously. Problem: An issue with testing multiple changes simultaneously is that it can be unclear which change form which author caused the failure when tests fail, as all changes from all authors included in the test can be at fault. Design: To solve this, a new automatic fault localization algorithm called GitFL is introduced, which combines state-of-the-art fault localization with version control history information for enhanced performance. GitFL was evaluated on a C++ repository at Adyen where tests are considered to be end-to-end. Findings: It showed that the addition of version control history information significantly increases the performance of fault localization for systems where multiple changes are tested simultaneously. Societal implications: This work provides insights on improved fault localization for these systems, which could enable organizations which develop these systems to speed up their testing and development processes. Originality: This work contributes by focusing on fault localization specifically for systems where multiple changes are tested simultaneously, which was not researched before.

In this thesis, we develop a new library for Agda named Attic, which allows us to create and compose proof tactics that can be used to generate terms through reflection. Such tactics can be converted to Agda macros, allowing them to be used in term positions where they can generate term solutions of the expected type. Tactics can make the development of proofs faster by making proofs easier to read and write.

This project can be seen as a sister project to Ataca, which is an earlier attempt at developing tactics that operate through reflection. Attic explores new mechanisms of operation, such as non-determinism with iterators to allow for multiple solutions, and the use of deferred unification, so that the final proof term is only fully constructed at the end of tactic evaluation.

To allow for the representation of both finite and infinite sequences that can be consumed step-by-step, we have implemented the iterator data type in Agda. Although iterators existed in other systems previously, an Agda implementation had not been made. These iterators underpin the branching mechanism in tactic instructions, and support operations that can be used to generate, transform and filter values.

Finally, we have implemented a number of tactics and operations that are commonly found in other proof assistants. We also compare the resulting library to the Ataca library and examine the differences in runtime for a small test case. While Attic is not yet a complete solution, we present new ideas that may be incorporated in future tactic systems.

Cyber-physical systems are complex systems constructed from different independent parts. A self-driving car is an example of a cyber-physical system where independent parts have to come together in order to result in a car that is able to drive by itself. The main challenge is finding failures within the interactions between the independent parts of the self-driving system. In this paper, we present a novel algorithm REWOSA, in order to detect these faults within the self-driving software. With the use of real-world roads extracted from Google Maps combined with a multi-objective genetic algorithm, we develop a new way to generate roads for testing self-driving cars. We evaluate this algorithm against a state-of-the-art multi-objective genetic algorithm using randomly generated roads using two different setups. Our results show that REWOSA is able to generate more failures than the baseline on both the setups, as well as create more complex roads. In return, REWOSA does create a large overhead due to the complexity of the real-world roads. However, this overhead is justifiable as we can detect more faults with the more complex real-world roads.

Visible Light Positioning (VLP) is an emerging field of research with several possible application. While most state-of-the-art VLP systems work with active modulation of light (switching lights on/off rapidly), this poses issues such as the flickering problem and excessive power consumption. In contrast, passive modulation of light (twisting/bending of light), with the properties of polarizers and birefringent materials, allows cost-effective modulation. This paper analyzes two birefringent materials - plastic (cling-wrap) and transparent adhesive tape - to test them for their usability in a visible light positioning system, in particular, the visibility range, hue-orientation mapping, and ambient light interference. These materials allow to create color patterns visible only to a camera. The patterns can encode data about identifiers of light anchors, while the color detected can be used to find the orientation of the receiver. It was observed that transparent adhesive tape gave much more reliable results, with a step-pattern-like hue-orientation mapping, and low errors ($\pm$ 5) on the hue value detected in the range of 30-250 cm from the light anchor, making it ideal for VLP.

Quantum computing is an emerging field with many promising future applications.
These include, but are not limited to, quantum machine learning, quantum cryptography and quantum chemical engineering.

Before these can be realised, obstacles, which arise due to scaling, need to be overcome.
To accomplish this, quantum processors must be built with low noise and high target gate fidelity rates.
By characterising quantum systems, possible sources of noise can be identified, and consequently, systems can be designed which effectively suppress noise.

Gate Set Tomography (GST) is a protocol developed for the characterisation of quantum processors.
In this research, we apply GST to nitrogen-vacancy (NV) centre systems.
We also construct a widget meant to visualise GST results in an intuitive manner.

Our research is based on twelve models, varying in the number of gates used, the initial state of the nitrogen nucleus, and whether an XY4 echo was applied after gates.
We use simulated and experimental models, and analyse these using the error generator, diamond norm and Nσ metrics.

We conclude that our simulated models capture sources of noise, as the proportion of stochastic errors shifts to Hamiltonian errors when we change our target model from the ideal model to the simulated ones.
We also conclude that the XY4 echo significantly reduces non-Markovianity, which arises due to coupling.
Furthermore, evidence which points to calibration faults is discovered within certain models.
Finally, we present the visualisation widget and show how it can be used to interpret results.

In the field of Visible Light Sensing, light sensors are used to extract information from objects which do not actively communicate any information. Previous research within this field proposed the system called SolAR, and proved the possibility of using a solar cell as both a power source and an activity sensor. A wrist mounted solar cell generates more energy than it uses during operation, while achieving a high classification accuracy for different activities. While the wearer performs different activities, the power output of the solar cell fluctuates. In turn, these fluctuations are used to recognise activities. To extend on the concept of SolAR, this paper introduces a prototype to obtain data from different activities while performing day-to-day tasks. During these activities, ordinary actions are performed to emulate natural circumstances. Analysis of this data initially shows no significant drop in accuracy when compared to SolAR. Further examination shows significant differences in mislabelling rates when comparing to the results of SolAR.