MSc Defences Winter 2025

Name of student(s)  

Jonas Wolpers Reholt

Study Programme  

Computer Science

Title  

Formally Verified Automatic Verification of eBPF Programs

Abstract  

This thesis addresses the challenge of achieving a formally verified automatic verification process for eBPF programs, a crucial component of modern Linux kernel extensibility. eBPF (extended Berkeley Packet Filter) enables highperformance, programmable extensions to the Linux kernel. However, its deployment in privileged kernel contexts necessitates rigorous safety guarantees to prevent malicious or faulty programs from compromising system security.

The thesis contributes a foundational step toward creating a fully formalized and verified eBPF verifier by leveraging the Isabelle proof assistant. This involves formalizing the semantics of eBPF programs and proving the soundness of key verification processes. By utilizing abstract interpretation the verifier is able to statically ensure compliance with critical safetly properties, such as bounded execution and memory safety. Moreover the project create a prototype formally proving handling of certain instructions in the verifier, paving the way for future enhancements.

This research builds on prior studies of the eBPF verifiers soundness and precision, offering new insights and tools to improve the reliability and efficiency of the eBPF technology stack. The findings contribute to the broader effort of using formal methods to prove safety of the kernel-level program security without compromising performance of the running program.

Supervisor(s)  

Thomas Philip Jensen

External examiner(s)  

Carsten Elmar Schürmann

Date and time  

09.01.2025 13:30-14:30

Room  

SCI-DIKU-HCO-01-0-029

Name of student(s)  

Rune Ejnar Bang Lejbølle and Kristoffer August Kortbæk

Study Programme  

Computer Science

Title  

Utilizing Tensor Cores in Futhark

Abstract  

Modern hardware has become more heterogeneous, and with the AI boom, specialized hardware for especially performing matrix multiplication has become readily available. In NVIDIA graphical processing units (GPUs), Tensor Cores allow for efficient execution of matrix multiplication routines that can significantly speed up AI and deep learning operations,
as well as other programs containing matrix multiplication.

However, programming for the Tensor Cores is not straightforward, and often requires adapting code to restrictions and performance guidelines unique to this hardware. The hardware is made more accessible through application specific libraries such as cuBLAS and cuDNN, but for more general use specialized CUDA or PTX code targeting the Tensor Cores
must be written. In order to ease the use of Tensor Cores in general, we propose to integrate the use of Tensor Cores into Futhark, a data parallel array language and highly optimizing compiler that generates efficient GPU code.

Our main contribution is to allow Futhark programs with matrix multiplication in an intragroup kernel to use the Tensor Cores. We evaluate the Futhark compiler output against handwritten CUDA programs using the Tensor Cores and the stock unmodified compiler on benchmarks such as the matrix multiplication routine from LU-Decomposition in Rodinia
[1], FlashAttention [2] like programs, and other matrix multiplication programs. The results show that our modified compiler is still considerably slower than handwritten implementations, but compared to the stock Futhark compiler we see speedups between 1.9× and 60×.

Supervisor(s)  

Cosmin Eugen Oancea

External examiner(s)  

Mircea Filip Lungu

Date and time  

10.01.2025 16:00-17:00

Room  

HCØ 01-0-S29 (PLTC-mødelokalet)

Name of student(s)  

Nathalie Gamliely

Study Programme  

Computer Science

Title  

Application of Generative Models in Block Copolymer Phase Discovery

Abstract  

This thesis explores the application of generative models, specifically Generative Adversarial Networks(GAN) and Denoising Diffusion Probabilistic Models(DDPM), in advancing block copolymer phase discovery. While powerful, traditional methods like Self-Consistent Field Theory(SCFT) suffer from limitations due to their reliance on accurate initial guesses and susceptibility to local minima. By leveraging machine learning, we
aim to address these challenges by introducing a computational pipeline that integrates generative models with SCFT to propose initial conditions efficiently. Our work focuses on bicontinuous and spherical packing
phases, validating GAN-SCFT pipelines and pioneering the application of DDPMs in this domain. Comparative analysis between GANs and DDPMs reveals distinct advantages and limitations, with GANs excelling
in convergence rates while DDPMs demonstrate potential for capturing diverse morphologies. Fourier and Principal Component analyses further elucidate structural periodicity and diversity in the generated phases.
This interdisciplinary approach underscores the transformative role of machine learning in computational copolymer science, setting the stage for discovering novel morphologies and materials.

Supervisor(s)  

Jon Sporring

External examiner(s)  

Melih Kandemir

Date and time  

16.01.2025 13:30-15:00

Room  

UP1-2-0-04 og 06

Name of student(s)  

Martin Inigo Aguayo and Eric Deng

Study Programme  

Computer Science

Title  

Designing and Developing a Search Tool for Football Tracking Data

Abstract  

This paper introduces a spatiotemporal model that analyzes football tracking data, focusing on player positions and movements to assist video analysts in identifying similar situations across or within football matches. Prior research has explored various aspects of football analytics using event and video data, often relying on general or black-box machine learning models. However, the dataset provided by DBU offers unique opportunities
to investigate areas that have not been explored in existing literature. The model we have developed effectively transforms raw positional tracking data into meaningful insights by integrating domain knowledge with advanced methods such as Earth Mover’s Distance (EMD) for spatial similarity and Dynamic Time Warping (DTW) for temporal alignment. A
dynamic weighting function further enhances EMD by emphasizing players near the ball, improving the relevance of similarity measures. Empirical evaluations, including feedback from professional video analysts, demonstrate the model’s capability to provide relevant and actionable recommendations, achieving an nDCG score of 0.56—significantly outperforming baseline approaches. While additional testing and optimization are needed to enhance real-world applicability, this tool represents a robust and practical solution for analyzing and identifying relevant sequences, enabling efficient and informed video analysis. Consequently, our solution streamlines the analysts’ workflow by reducing the time and effort needed to find relevant match situations.

Supervisor(s)  

Jon Sporring

External examiner(s)  

Melih Kandemir

Date and time  

16.01.2025 15:00-16:30

Room  

UP1-2-0-04 og 06

Name of student(s)  

Nicolai Jonathan Epshtein

Study Programme  

Computer Science

Title  

Real-Time Rendering of Granular Materials Based on Light Transport Simulation

Abstract  

In this thesis, we develop a method for real-time rendering of granular materials based on light transport simulation. We specifically focus on how to efficiently and realistically render granular materials modeled as an aggregation of individual grains. The proposed method consists of two separable parts that are used in union to describe the full scattering behavior of the granular material, applicable directly a in real-time rendering pipeline.

The first part introduces an approximate method for intra-grain scattering for single-grain representation, by modeling the complex light transport within the grain as a precomputed aggregation of scattering events. We define the singlegrain shading model as an eight-dimensional grain scattering distribution function (GSDF). Under multiple assumptions, we show how to reduce the 8D GSDF to approximations of both 4D, 2D, and 1D functions. We further show how to tabulate and precompute the GSDF using measured data acquired from light transport simulation. Additionally, for use in the second part of the method, we show how to
apply a continuous approximation of the 1D GSDF.

The second part of the method is a physics-based approximation for modeling multiple scattering between grains within a granular material. To approximate intergrain scattering, we utilize and adapt the dual scattering approximation, originally designed for hair rendering, and show how to derive it for use in real-time rendering of granular materials.

To test and validate the proposed method, we develop a reference implementation and compare the results with path tracing references.

The results show that the 4D GSDF is able to closely approximate the path
tracing references, while the lower dimensional approximations also tend toward the path tracing references as the viewing distance increases. While the 4D GSDF is able to closely approximate intra-grain scattering of a given grain type, it is shown that the further reduced approximations struggle to handle grains exhibiting prominent specular reflection, as all backscattering light paths of the grain are combined into a single term.
The results also show that the dual scattering method is able to closely approximate and reproduce the effects of multiple scattering between grains, showing proper occlusion and translucency of grains within the granular material, matching that of path tracing references. However, we also observe that some intensity is lost in the approximation. We likewise observe similar issues of specular reflection of grains as discovered for the GSDF, as specular reflections are smoothed in the continuous
approximation of the GSDF. To reduce the errors arising from specular reflections of grains we show that it is possible to incorporate an additional specular reflection factor during rendering, where we likewise also propose extending the continuous approximation of the GSDF with additional separate scattering lobes.

Supervisor(s)  

Francois Bernard Lauze and Jeppe Revall Frisvad
Co-supervisor: Jakob Gath

External examiner(s)  

Henrique Galvan Debarba

Date and time  

16.01.2025 15:00-16:00

Room  

Image Hot Room 3.2.02A

Name of student(s)  

Janne Brøgger and Nicolaj Richs-Jensen

Study Programme  

Computer Science

Title  

Nonobtuse Triangulation of Polygons and Planar Straight Line Graphs Including Steiner Points

Abstract  

We present an implementation of a linear-size nonobtuse triangulation algorithm for polygons by Bern et al. [6], applying an alternative approach that completely avoids the use of General Voronoi Diagrams. This is
achieved at the cost of increased running time, which is O(n2).

Additionally, we present a method for constructing a nonobtuse triangulation of planar straight-line graphs relying on the algorithm for polygons. Our approach is significantly simpler than - what we think is - the
only existing algorithm for this problem, proposed by Bishop [7]. Our method does not guarantee any bounds on either the number of triangles or the running time, however in practice it shows promising results.
We present an implementation of this method, which is built upon the aforementioned implementation of nonobtuse triangulation of polygons.

Finally, we also present two tools for drawing a polygon, and drawing a planar straight-line graph to ensure that the reader can explore the implementations for triangulating arbitrary instances. The drawing tools offer a wide range of useful features to enhance the overall experience.

Supervisor(s)  

Mikkel Vind Abrahamsen

External examiner(s)  

Thore Husfeldt

Date and time  

24.01.2025 10:15-11:30

Room  

HCØ Aud. 7

Name of student(s)  

Patrick Mørch

Study Programme  

Computer Science

Title  

HTPL: A High-level Domain Specific Language for Expressive Trust Relations in the Maritime Domain

Abstract  

The maritime domain consist of several large separated organizations and
companies responsible for shipping, oil-drilling and other activities in the
ocean. By the scattered nature of the domain, there is a need for an efficient and specific authorization to be implemented. This is typically
done using trust management systems, such as Public Key Infrastructures (PKI), though traditional PKIs lack functionality for specifying trust. The firm P3KI GmbH, aims to solve these issues by offering a decentralized PKI, P3KI Core, which bases authorization on policies defined in a Trust Policy Language (TPL). P3KI Core is optimal for use in the maritime sector, as it offers a decentralized system with functionality such as offline usage and specific trust.

P3KI Core’s use of a low-level TPL makes interacting with the PKI susceptible to errors. This paper aims to to build a High-level Domain Specific Language (DSL) on top of TPL, which makes interactions with PKI less error prone and improving the overall user experience by abstracting away complexity. This is accomplished by analyzing the needs of the domain and examining similar languages. Based on this analysis, a design is defined to meet the domain’s requirements. Finally, the implemented design is evaluated and discussed.

The goal of the paper is achieved through the design and implementation of the language HTPL, which implements several operations for
efficiently specifying trust relationships. As such, we have found that a
High-level Trust Policy Language can successfully be implemented on top
of TPL to aid in efficiently defining trust relationships. This language
could be further developed for practical use in the maritime sector.

Supervisor(s)  

Michael Kirkedal Thomsen

External examiner(s)  

Birger Andersen

Date and time  

24.01.2025 13:00-14:00

Room  

HCØ-01-0-027/029

Name of student(s)  

Pedram Bakhtiarifard

Study Programme  

Computer Science

Title  

On the Feasibility of Topological Complexity Measures in Nonconvex Optimization

Abstract  

Modern deep learning optimizers operate in high-dimensional, nonconvex landscapes characterized by saddle points, elongated valleys,
and intricate global structures. While state-of-the-art methods primarily rely on local gradient and curvature signals, recent theoretical and
empirical insights suggest that these may not fully capture the complex global geometry governing training dynamics and generalization
behavior. This thesis investigates the feasibility and implications of incorporating topological complexity measures - derived from persistent
homology - into the core of iterative optimization algorithms.
We introduce two novel optimizers that integrate global topological
invariants into their update rules. The first, Filtration-Level Momentum (FL-Mom), adapts step sizes based on a topological complexity
measure computed from neighborhoods in parameter space. The second, TopoPath, selects among candidate update directions by evaluating their associated topological complexity and choosing paths that
lead into simpler, more navigable regions of the loss surface. Both
methods employ dimensionality reduction and stability theorems to
ensure computational tractability and theoretical soundness. Under
standard nonconvex convergence assumptions, we establish that these
topology-informed approaches retain convergence guarantees, thereby
complementing rather than replacing local heuristics.
To assess their practical value, we benchmark these topological methods
against robust baselines - including SGD with Nesterov momentum,
QHAdam, and YellowFin - on canonical problems such as Rosenbrock,
Ackley, Rastrigin, Himmelblau, across multiple dimensions. The results
show that while topological cues can sometimes facilitate navigation of
globally deceptive landscapes, particularly at higher dimensionalities
or in scenarios with subtle plateau structures, they do not universally
outperform well-tuned adaptive optimizers. In problems with uniformly distributed local minima or relatively mild complexity, standard
approaches remain highly competitive, and topological insights offer
minimal gains.
These findings highlight the nuanced role of topological complexity in
deep learning optimization. While not a universal cure-all, the integration of persistent homology-based measures opens a research direction
for developing hybrid, problem-specific strategies that blend local and
global signals. This thesis thus takes a step towards understanding
when and how topological complexity can enhance the training of
deep neural networks, and is a springboard for future refinements and
broader applications in large-scale, real-world optimization tasks.

Supervisor(s)  

Raghavendra Selvan

External examiner(s)  

Lee Herluf Lund Lassen

Date and time  

29.01.2025 14:00-15:00

Room  

UP1-2-0-15

Name of student(s)  

Axel Rove

Study Programme  

Sundhed og Informatik

Title  

Artificial Intelligence - Present or future?

Abstract  

This thesis explores the potential of artificial intelligence to enhance diagnostic processes and patient care in the healthcare sector while also addressing the challenges and ethical considerations necessary for an successful implementation. Through a comprehensive analysis of literature and case studies, the paper identifies AI's strengths, weaknesses, and future opportunities in the healthcare domain.

AI holds the potential to revolutionize the healthcare sector by increasing the accuracy of diagnostic processes, reducing errors, and enabling early disease detection through advanced image recognition and patient data analysis. The technology also supports personalized medicine by
tailoring treatment plans to individual patients based on genetic data, lifestyle factors, and medical history. Furthermore, AI can streamline administrative tasks such as record-keeping, scheduling, and billing, freeing up time and resources for healthcare professionals.

Despite these advantages, AI faces significant challenges. Ethical issues such as data security, patient confidentiality, and the risk of algorithmic bias are critical. The lack of transparency in AI decision-making creates additional uncertainty and can diminish trust among both healthcare
professionals and patients. Implementation also requires substantial resources and expertise, as well as clear regulatory frameworks to ensure responsible usage.

The discussion highlights the importance of a holistic approach to AI implementation, balancing the technology's potential with its social, ethical, and practical challenges. Recommendations include strengthening data security through technologies like differential privacy, reducing algorithmic bias via representative datasets, and establishing robust regulatory frameworks such as those proposed in the EU’s AI Act.

The thesis concludes that AI has transformative possibilities to enhance the healthcare sector, but its success depends on a responsible and strategic approach. By addressing technological and ethical challenges, AI can contribute to a more efficient, equitable, and patient-centered healthcare system. Ensuring a sustainable future for AI in healthcare requires ongoing evaluation and collaboration between technology developers, healthcare professionals, and policymakers.

Supervisor(s)  

Erling Carl Havn

External examiner(s)  

Jens Pedersen

Date and time  

10.01.2025 10:00-11:00

Room  

SCI-DIKU-HCO-01-0-029

Name of student(s)  

Noah Brunken Syrkis

Study Programme  

IT and Cognition

Title  

Mechanistic Interpretability on multi-task Irreducible Integer Identifiers

Abstract  

This paper investigates how neural networks solve multiple related
mathematical tasks simultaneously through mechanistic interpretability. A trans, former model is trained on 29 parallel tasks, each predicting remainders when dividing two,digit base,113 numbers by all primes less than 113. This setup spans task complexity from binary classification (division by 2) to 109,way classification (largest prime less than 113). Further, the model, trained using gradient filtering to accelerate generalization, achieves perfect accuracy across all tasks. Embedding
analysis, singular value decomposition, and Fourier analysis of neuron activations reveal complex internal representations. The model initially solves simpler tasks (modulo 2, 3, 5, and 7) before developing a shared strategy for the remaining tasks.
The increased number of active frequencies in neuron activations suggests a phase where additional circuits form during generalization, some facilitating learning but not present in the final solution. Findings also confirm that amplifying slow,moving gradients significantly accelerates generalization.

This study shows that multi,task learning shapes the development of internal mechanisms in deep learning models, offering insights into how these models inter, nalize algorithms across tasks. Future research could automate circuit discovery and explore variations in multi,task learning setups. The project repository is available at https://github.com/syrkis/miiii.

Supervisor(s)  

Anders Søgaard

External examiner(s)  

Zeljko Agic

Date and time  

08.01.2025 10:00-11:00

Room  

Online