Alessandro Bruni

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.