The Language Server Protocol (LSP) is a protocol that standardizes the way Integrated Development Environments (IDEs) and text editors communicate with language servers to provide language-specific features like autocompletion, go-to-definition, and diagnostics. While LSP has been widely adopted by mainstream programming languages, its adoption in dependently typed languages has been slower due to the unique challenges posed by their complex type systems and interactive theorem proving capabilities. This thesis explores the potential of LSP for enhancing the development of dependently typed programs, focusing on the Agda programming language. We present the implementation of a prototype LSP server for Agda that leverages scope checking to provide fast and responsive IDE features. We evaluate the performance of the prototype and compare its feature completeness with existing Agda development tools. Our findings demonstrate that scope checking can serve as a foundation for implementing efficient LSP features in Agda, offering a promising direction for improving the tooling and overall development experience for dependently typed languages.

Type annotations in Python are an integral part of static analysis. They can be used for code documentation, error detection and the development of cleaner architectures. By enhancing code quality, they contribute to the robustness, maintainability and comprehensibility of codebases. Tools like static type checkers use type annotations to detect bugs early, with some type checkers like Pyright being capable of inferring annotations statically from source code.

This thesis uses an innovative approach to further enhance type annotation coverage in Python codebases by using a combination of machine learning predictions and combinatorial search. To do this, PyHintSearch was developed. PyHintSearch constructs a search tree to which a depth-first search is applied to systematically explore potential combinations of predicted type annotations and validate them using feedback from the Pyright static type checker. Ultimately, the goal is to identify a branch containing a valid combination of type annotations. These annotations can then be integrated into Python code, thereby enhancing the type annotation coverage, which leads to improved static analysis and ultimately better code quality.

PyHintSearch's effectiveness is evaluated based on type annotation coverage and correctness, performance, and practical usability. Experimental results demonstrate different improvements in type annotation coverage, depending on the machine learning model used for type inference. Type4Py showed an improvement of 62.45% and TypeT5 of 79.93%. The precision of type annotations from these models are 0.36 and 0.51, respectively. Performance-wise, PyHintSearch can efficiently explore the exponential search space, annotating 16 diverse projects, ranging from small to large, in approximately 13.75 hours when using the Type4Py model. Regarding practical usability, the impact of type annotations on downstream program analysis is examined through the generation of call graphs. The additional information that type annotations provide can be used to refine the call graph by eliminating irrelevant calls to make it more precise.

Open source software (OSS) vulnerabilities form a real threat to the security of software that employs them.
Efforts to mitigate these risks exist in the form of dependency check tools, however these often suffer from imprecise warnings due to the utilization of only metadata.
This thesis investigates the use of CVEs in a more code-centric approach and the effect this has on the detection of vulnerability reachability in OSS dependencies.
This paper proposes an automated approach to enrich CVEs with preciser code-level information by leveraging references such as patches, repositories, and vulnerability databases.
This thesis then heads out to investigate the impact on accuracy of various (novel) approaches in terms of granularity (packages, classes, methods) and in terms of source for the patch information (link to a commit, PR of commits, or binary diff).
Our experimental results show that these code-centric approaches significantly improve vulnerability detection, achieving higher precision compared to traditional dependency checkers.
Additionally, we present the trade-offs between the different methods, highlighting their strengths and weaknesses.
Through this work, we show how utilizing code information into dependency analysis can substantially enhance the detection of vulnerable code paths, offering more accurate risk assessments in software ecosystems.

Insects such as Diptera are capable of highly complex aerial maneuvers and rapid responses to environmental stimuli, making them a subject of interest for studies in flight dynamics and motor control. To accurately quantify these movements, high-speed cameras are employed, capturing footage at 5000 frames per second. This results in a vast amount of data, necessitating the development of automated analysis models. In this work, we present a segmentation model specifically designed for the wings of Diptera species, aiming to track their wingbeats with high precision. The model’s performance was evaluated on species included in the training set as well as on species only included in the testset, allowing us to assess its generalization capabilities. Our results show that the model achieves a 95th percentile error of 7.8 pixels, while operating at a speed 2500 times faster than manual human analysis. This significant improvement in speed highlights the potential for our model to facilitate large-scale, high-speed analysis of insect flight, with implications for both biological research and bio-inspired engineering applications.

This research explores the size variations of artifacts in Maven Central, a repository containing a large collection of Java artifacts. This analysis sheds light on the coding habits and dependency management ecosystems within Maven Central, emphasizing the importance of managing artifact sizes effectively. It also provides valuable insights to library maintainers and clients who want to download libraries. For example, we can determine the average amount of space required to download 100 libraries.
The analysis is done by selecting a single version for each artifact in Maven Central and extracting metadata from the corresponding files.
The results reveal that the average size of an artifact is 1447 KB, although this average is heavily influenced by a few exceptionally large artifacts. Approximately 86% of the artifacts have a size smaller than 400 KB, indicating that the majority of artifacts are relatively lightweight.
The large artifacts identified in the analysis are predominantly attributed to two categories. The first category contains extensive projects with a substantial number of files, while the second category includes machine learning or big data projects that include massive data files.

Inductive logic programming is a technique that generates logic programs which keep to a given specification using a background knowledge. We propose a new task in the field of pro- gram synthesis called Time-gated Partition-selection Inductive Logic Programming, consisting of splitting the background knowledge into partitions and selecting only the relevant partitions to a given set of examples. In order to show an initial direction of research and demonstrate the effectiveness of the approach, we have constructed a set of partitioning functions and a selection function. These were implemented using existing graph clustering and community detection algorithms applied to static call graphs of existing programs in the target language and using a linear time evaluation selection function. By comparing the inductive logic programming approach Popper to a version of Popper with its search space reduced using this technique, we show that these partitioning- and selection functions can improve the generated programs on three out of four different domains. Finally we show that there is a difference in partition quality by comparing the results to a random partitioning function. This work establishes background knowledge partitioning- and selection as a useful tool in program synthesis research.

Cloud computing and storage solutions have been credited with increasing competitiveness through cost savings, greater flexibility, elasticity and optimal resource allocation. However, the data outsourced to the cloud may contain private information that must be protected from misuse. In such cases, the data can only be outsourced after encryption. Graphs are widely used to model and represent data in various applications, including geographic information systems. Yet performing the shortest path algorithm over such encrypted outsourced graphs represents a challenge. Current approaches rely on trusted third parties, employ weaker security measures, or treat the cloud as a storage medium rather than addressing the algorithmic complexities directly. This makes the adoption of such protocols difficult in practice.

In this work, we develop two privacy-preserving navigation protocols to compute the shortest path over encrypted outsourced graphs, under different security and efficiency guarantees. The first protocol enables one to retrieve the shortest path in an oblivious manner, that is, without the cloud learning any information about the outsourced graph or the returned path. The second protocol assumes that the topology of the outsourced graph is public knowledge, and obtains retrieval times orders of magnitude faster. The evaluation results on a proof-of-concept implementation indicate that the condition number of the node-incidence matrix of the graph being outsourced serves as a determining factor for the number of iterations. Dense graphs exhibit a low condition number. In such cases, the high number of iterations required for convergence, quadratic time complexity with respect to the number of edges in the graph, and the inherently slow homomorphic operations results in impractical retrieval times. Conversely, sparse graphs allow for trivial resolution of shortest paths within a single iteration.

Continuous Integration (CI) is a software development technique that enhances software quality and development efficiency, but its implementation usually depends on the project's context. This creates an opportunity for studying real-world CI projects on GitHub, focusing on their CI metrics and best practices. In this paper, we explore various methods to extract the topics from CI software projects on GitHub. This data can then be used to group projects and facilitate an in-depth analysis within specific contexts and application domains, such as CI build success rates in machine learning or React Native projects. We explore the definition of a software topic, as it shows significant granularity variations in related studies. We examine existing tools and other potential topic modeling approaches, compare varying types of textual data from GitHub that could be used as inputs for these tools, and report on interesting insights from initial trials with the developed tool. Our research led us to use GitHub topic labels as topic definitions due to their relevance and prior research focus. We also evaluated three topic extraction tools - LASCAD, a Multi-label Linear Regression classifier, and ChatGPT - incorporating the last two into our CI project mining tool. Additionally, we included two tool-independent approaches: GitHub's search function with the ability to filter repositories by topics and existing project topic labels. Lastly, to test the practicality of the tool, we mined 4899 public repositories and briefly investigated workflow metrics of projects grouped into six arbitrary topics.

Continuous Integration (CI) systems automate the building, testing, and possibly more. However, it is still unclear how CI should be implemented in different contexts. Therefore, this paper tries to answer the question "What metrics can be used to describe project activity", as part of a bigger study. We mined information from 500 repositories and then applied several analysis techniques to find out whether a metric can be used to describe activity or not. Among the results, we show that the activity around a release date increases, and that Java is a way more active language than other languages, with the highest amount of commits, closed pull requests, contributors, issues, and releases.

As the sharing of machine learning (ML) models has increased in popularity, more so-called model zoos are created. These repositories facilitate the sharing of models and their metadata, and other people to find and re-use an existing model. However, the metadata provided for models is insufficient, with little focus on practical aspects of a model such as performance and limitations. This leaves model zoos to provide little functinality beyond the sharing of existing models, and potential users unable to find an optimal model for their needs. In this thesis we focus on the reporting of model performance, and aim to answer two questions: (1) What are the limitations of model performance reporting found in current model zoos, and (2) How can we provide rich, comparable performance metadata for these models. As a result, we have created a framework which can be used to create a benchmarking system for ML models. Our framework enables the automatic evaluation of models from any source, and through its design encourages the collection of rich and comparable performance metadata for those models. To demonstrate the effectiveness of our framework, we have created a benchmarking system and evaluated 1215 models from existing model zoos, along with a new interface to view this new metadata, and have enabled new use-cases such as the performance comparison of ML models.

Recent large scale cyber security incidents such as the Equifax data breach, where the personal information of around 160 million Americans leaked, demonstrate the current risk of security vulnerabilities libraries which software projects depend on.
The usage of libraries forms an integral part of modern software development and is a widespread practice across software projects.
Libraries make it possible to use proven implementations of certain functionalities without duplicating it.
However, this means the usage of libraries creates a set of dependencies for software projects.
While using libraries allows for increased development speeds by reusing existing code, these dependencies can also propagate problems which exist in dependencies.
Therefore, a security vulnerability in a dependency can have a major impact on the software project as a whole.

Currently, there are analysers which perform a high level analysis which can identify vulnerable dependencies.
However, these analysers are limited to the package level, where either a whole library is considered vulnerable or safe.
In reality, the situation is often more nuanced, where only certain functions of a library pose a security risk.
Considering the growing number of dependencies of software projects and the increasing number of vulnerability disclosure, the dependency update management process is currently a difficult task.

Therefor a more fine-grained type of analysis could help developers in identifying and mitigating actual security risks.
In this thesis, we propose a new risk modelling approach which uses fine grained analysis to concentrate these efforts as best as possible and increase security of software applications.
Further we perform an extensive evaluation to compare it to existing risk approaches to investigate the accuracy of the proposed approach.
We find that the new risk model is more accurate in prioritising risk mitigation strategies, with an average increase of 8% of current state of the art risk models.
The model does require function level vulnerability information which does not exist for all disclosed vulnerabilities and is an active area of research.

Online controlled experimentation (OCE), also called A/B testing, is an often used tool in industry to determine if deploying changes into production is the right decision to make. Running experiments has shown an immense impact to the revenue of companies in industry, however this type of experimentation comes with a lot of pitfalls, of which some that can invalidate the entire experiment. This thesis describes the impact these pitfalls have on the work of experimenters at ING, a global bank, by performing informal interviews with practitioners and performing a survey with 52 participants. Next, building on existing solutions, a set of solutions is proposed to solve these pitfalls. To determine if these solutions solve the problem and will help the experimenter, these solutions are validated in the same survey. This thesis shows that experimenters are well informed about the existence of pitfalls and believe that almost all should be resolved, with the exception of competitor safety, which is believed to not be important. There are many promising solutions to these pitfalls which experimenters rate as helpful. The best rated solution was ”Enforcing the correct experiment duration”. Almost all respondents perceived the solution to (slightly) help the experimenter in performing their experiments. Finally, this thesis creates a roadmap for evaluating these solutions in a real-world scenario.