Projects
How to find a good thesis topic?
The two most important things for finding a good thesis topic is to find a topic that excites you and your supervisor, and that you have the competencies to succeed in.
To help you find a good thesis topic you can read a list of concrete thesis topics that I would be excited to supervise, and a list of past theses from which you can take inspiration. You can pick a topic from my list or propose a topic of your own.
Project ideas
Verified machine learning
Where traditional software development is akin to giving precise instructions, or rules, to a computer, machine learning lets the computer learn the target function from data. While convenient, one big issue with this approach is that it’s really hard to check that a function behaves as intended if it is based on a neural network. I am interested in using software verification techniques on machine learning systems to guarantee that such systems behave as intended, by using a mix of logical specifications, programming language theory, and machine learning theory. This work can focus either on the infrastructure (the tools themselves, or their mathematical foundations) or on specific case studies (we are currently verifying network intrustion detection systems and autonomous driving controllers, but I’m interested in expanding the range of applications). One of the tools I use (and contribute to) is the Vehicle language.
NLP for Software Verification
I’m interested in integrating LLMs with interactive theorem provers, specifically the Rocq prover. There are plenty of ideas to explore, from generating good documentation for existing developments, to automating theorem proving, translating proofs between different ITPs, solving frontier math problems, integrating LLMs in learning environments for proof assistants.
Verified software systems and cryptographic protocols
I am mainly interest in analysis using the Rocq prover and the MathComp-Analysis project, to which I contribute. I have a few targets currently in mind: within voting protocols, I’d like to analyze risk limiting audits, a statistical procedure that gives a confidence interval to check that elections have not been tampered; I’d like to analyze other sort of statistical procedures, like the multi-armed bandit algorithm. I have also experience analyzing security protocols, and am interested in doing verification using formal frameworks such as SSprove.
Past theses
Here is a list of past thesis titles, I hope this gives you some insight in the kinds of theses that I supervise. Feel free to ask about some topics.
- Developing Robust Neural Network Models for Network Intrusion Detection, Vladislav Konjusenko and Oleksandr Adamov (BDS, 2025)
- Exploring PAC-Learnability of decision stumps in Coq (SWU, 2024)
- Machine learning robustness using Vehicle (BDS, 2024)
- Building training material and challenges on fuzzing and symbolic execution (SWU, 2024)
- Building a linter for finding security vulnerabilities in Dockerfiles (SWU, 2024)
- Visualizing security protocols as choreographies (SWU, 2023)
- Human detection of AI generated images (KCS, 2023)
- EMV payment attacks (KCS, 2023)
- Building a platform for running CTF competitions (SWU, 2023)
- Implementing Apachi, a conference management system (SWU, 2022, 2024)
- Implementing LoRaRatchet, a security protocol for IoT devices (KCS, 2022)
- Compiling security choreographies to executable code and ProVerif models (KCS, 2022)
- Hacking CAN bus vehicle health monitors (SWU, 2022)
- Finding zero day vulnerabilities in the Linux kernel using the CodeQL code scanning tool (SWU, 2022)
- Creating cybersecurity training material for highschool students (KSD, 2022)
- LoRaRatchet, a security protocol for IoT devices with post-compromise security (KSD, 2021)
- Threat assessment for LoRaWAN devices in offshore wind energy (KSD, 2021)
- Using the angr.io framework to find information flow vulnerabilities in Unix binaries (KCS, 2021)
- Security analysis of the OSCORE secure transport protocol for IoT (BSc, 2021)
- Extending session types to model security properties (KCS, 2021)
- Mitigating timing attacks on network traffic (MSC, 2021)
- Apachi - an Accountable, Secure and Fair Approach to Conference Paper Submission (KCS, 2020)
- Scanning the Danish internet to determine the state of Danish cybersecurity (SWU, 2020)
- Detection of botnets through the use of Honeypots (SWU, 2020)
- Formal Verification of the Firefox Sync Protocol, Spring 2019
- Security Analysis of a Smart Heat Meter, Spring 2019
- CityRun: A combined running- and sightseeing app, Spring 2019
- Decentralized certificate authority as a blockchain application, Spring 2019
- Extending Session Types to Model Security Properties, Spring 2019
- Formal Verification of Object Security for Constrained RESTful Environments (OSCORE), Spring 2019
- Formal verification of Certificate Transparency, Spring 2019
- Verification of privacy in Bingo Voting, Spring 2019
- Zero-knowledge proofs on the GPU for voting, Spring 2019
- From Applied Pi Calculus to Linear Logic, Fall 2018
- Formal analysis of EDHOC, a protocol for IoT secure communication, Theis Grønbech Petersen and Thorvald Sahl Jørgensen, Spring 2018
- Security analysis for smart door lock, Steffen Mogensen, Spring 2018
- Deduplicated Storage Systems: Trade-offs between security and efficiency, Emma Arfelt Kock, Fall 2017
- Verifying Selene in Tamarin, Eva Drewsen, Spring 2017
- Voting Protocol in Ethereum, Adrian Brink, Spring 2017
- Transparent authentication with wearable devices, Jacob Cholewa and Rasmus Wismann, Spring 2017
- Hacking WinVote machines, Florin Vasile and Andreas Nielsen, Fall 2016