For students

We supervise projects in the following areas.

If you are interested contact the potential supervisors directly.

Patrick Bahr

Patrick supervises projects related to compilers, type systems, functional programming, and formal verification. He is interested in topics such as functional reactive programming, the design and implementation of advanced type systems, compiler construction, and correct-by-construction compilers using formal methods.

More information including project ideas and previously supervised theses.

Jesper Bengtson

Jesper supervises projects in the area of formal verification, focusing on ensuring the correctness of software systems. His interests include developing frameworks and tools for verifying programs, prototyping new programming languages, and applying interactive proof assistants like Coq. He encourages projects that address real-world challenges in software reliability, such as verifying critical systems or exploring the boundaries of current verification techniques. Students interested in the intersection of programming languages, formal methods, and software correctness are welcome to contact him for supervision.

Alessandro Bruni

Alessandro supervises projects at the intersection of security, formal methods, and machine learning. His supervision covers areas such as training safe robot controllers using formal specifications, formalizing probability theory in Coq, analyzing and compiling secure protocols, and hacking projects for highly motivated students. He also shares examples of past theses to help students find inspiration and is open to discussing new and challenging topics within his areas of expertise.

Marco Carbone

Marco supervises projects related to the theory and practice of concurrency, semantics, type systems, and linear logic, with a particular focus on session types, the pi-calculus, and choreographies. He is interested in both foundational and applied aspects, including the mechanisation and verification of concurrent systems, probabilistic models, and secure communication protocols. Students keen to explore advanced topics in programming languages, formal methods, or concurrency theory are encouraged to contact him, especially if they are interested in research-oriented projects or contributing to ongoing research initiatives.

Rosario Giustolisi

Rosario is always interested in supervising new thesis projects and welcomes students with a passion for security, privacy, and formal methods. Some example topics include: feasibility studies of typosquatting attacks in forums and Q&A websites (such as Reddit, Stack Overflow, or Quora), improving password filters by enforcing random-looking passwords, usability studies of coercion-resistant voting systems, and the design and development of secure applications for decision systems (including e-voting and exams). Other areas of interest are the design and verification of accountability systems (like Google’s Certificate Transparency, Ethereum’s proof-of-stake, or voting systems) and the security analysis of socio-technical systems for fun and profit (such as transport tickets, car sharing, bike rental apps, or vending machines). Students are encouraged to reach out to discuss these or other related topics.

Rasmus Møgelberg

Rasmus supervises projects in the theory and implementation of programming languages. He is particularly interetested the design of advanced type systems, such as those used for functional reactive programming, language based security, automatic differentiation, systems with dependent types, as well as other features. He is also interested in the use and implementation of proof assistants, and more theoretical topics in logic, category theory and mathematics in general.

Willard Rafnsson

Willard supervises student research and thesis projects that align closely with his research interests and have the potential to result in a research publication. He is selective and only takes on projects he is highly enthusiastic about. Students interested in working with him should ensure their interests overlap with his research agenda and are encouraged to arrange a meeting to discuss potential topics. Willard’s current and past supervision covers areas such as server hardening automation, formal verification of security properties, binary analysis for vulnerabilities, automated vulnerability fixing in JavaScript libraries, emulation, privacy risk analysis, and information-flow security.

Carsten Schürmann

Carsten supervises projects in logic in computer science, logical frameworks, type theory, theorem proving, computational logic, and programming languages (both functional and logic programming). He is particularly interested in formal methods, proof assistants, and the development of logical frameworks such as Twelf and Delphin. Carsten welcomes students who are interested in foundational aspects of programming languages, formal verification, and applications of logic to real-world systems, including secure and trustworthy elections. He encourages students to propose research-oriented projects that align with his expertise in computational logic, formal digital libraries, and the intersection of logic and software engineering.