Alessandro Bruni

Current Courses

Past Courses

Thesis Supervision

I regularly supervise bachelor and master thesis projects in formal methods, security, and machine learning verification.

Looking for a thesis project? I’m recruiting students for paid thesis projects in the DIREC-funded project Robust Network Intrusion Detection. Topics span datasets, formal verification, differentiable logics, and privacy-preserving ML. Find out more →

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.

You can pick a topic from the list below or propose a topic of your own. The past theses section also gives a sense of the range of topics I supervise.

Project Ideas

Robust Network Intrusion Detection (DIREC project). I am leading a DIREC-funded Catalyst project on training robust network intrusion detection systems using differentiable logics. We have paid thesis positions available across four research themes: datasets, rules & training, differentiable logics, and privacy-preserving ML. See the project site for details and how to get involved.

Verified machine learning. Using software verification techniques on machine learning systems to guarantee they behave as intended, through logical specifications, programming language theory, and machine learning theory. This can focus on the infrastructure (tools and mathematical foundations) or specific case studies (network intrusion detection, autonomous driving controllers). One of the tools I use is the Vehicle language.

NLP for Software Verification. Integrating LLMs with interactive theorem provers, specifically the Rocq prover. Ideas range from generating documentation for existing developments, to automating theorem proving, translating proofs between ITPs, solving frontier math problems, and integrating LLMs in learning environments.

Verified software systems and cryptographic protocols. Analysis using the Rocq prover and MathComp-Analysis. Current targets include: risk-limiting audits for voting protocols, statistical procedures like the multi-armed bandit algorithm, and security protocol verification using frameworks such as SSprove.

Past Theses

Here is a list of past thesis titles — feel free to ask about any topic.