Skip to main content

MSc in Mathematics and Foundations of Computer Science - Student projects

Suggested projects

Project Supervisors Parts Description
Model learning and verification Alessandro Abate, Daniel Kroening

This project will explore connections of techniques from machine learning with successful approaches from formal verification. The project has two sides: a theoretical one, and a more practical one: it will be up to the student to emphasise either of the two sides depending on his/her background and/of interests. The theoretical part will develop existing research, for instance in one of the following two inter-disciplinary domain pairs: learning & repair, or reachability analysis & Bayesian inference. On the other hand, a more practical project will apply the above theoretical connections on a simple models setup in the area of robotics and autonomy.

Courses: Computer-Aided Formal Verification, Probabilistic Model Checking, Machine Learning

Precise simulations and analysis of aggregated probabilistic models Alessandro Abate

This project shall investigate a rich research line, recently pursued by a few within the Department of CS, looking at the development of quantitative abstractions of Markovian models. Abstractions come in the form of lumped, aggregated models, which are beneficial in being easier to simulate or to analyse. Key to the novelty of this work, the proposed abstractions are quantitative in that precise error bounds with the original model can be established. As such, whatever can be shown over the abstract model, can be as well formally discussed over the original one.

This project, grounded on existing literature, will pursue (depending on the student's interests) extensions of this recent work, or its implementation as a software tool.

Courses: Computer-Aided Formal Verification, Probabilistic Model Checking, Machine Learning

Classical simulation of quantum systems Jonathan Barrett


For many information theoretic tasks, an advantage can be gained if quantum systems are used as the basic carrier of information, rather than classical variables. For example, it may be the case that with quantum systems, fewer resources are required. The project will investigate the classical simulation of quantum systems in simple scenarios in which quantum systems are communicated from one party to another, or in which quantum systems are measured to produce correlated outcomes. The aim is to compare the resources required by the classical simulation with those required when quantum systems are used.


Linear algebra. A student taking this project should also be taking the Quantum Computer Science course. Some extra reading to cover the basic formalism of quantum theory would be an advantage.

Device-independent quantum cryptography Jonathan Barrett


One of the most successful applications of quantum information science is quantum key distribution, which enables separated parties to send secret messages, with security guaranteed by the laws of quantum theory. The mysterious phenomenon of “quantum nonlocality”, wherein two quantum systems appear to influence one another even though they are separated in space, can be used to design a particularly strong kind of key distribution protocol. The idea is that the honest users do not need to trust that their quantum devices are behaving as advertised, or even that quantum theory is correct. The project will explore the relationship between different kinds of nonlocality and the possibilities for secure communication.


Linear algebra. A student taking this project should also be taking the Quantum Computer Science course. Some extra reading to cover the basic formalism of quantum theory would be an advantage.

Towards Tractable Strategic Reasoning in Strategy Logic Julian Gutierrez

Strategy Logic (SL) is a temporal logic to reason about strategies in multi-player games. Such games have multiple applications in Logic and Semantics, Artificial Intelligence and Multi-Agent Systems, and Verification and Computer Science. SL is a very powerful logic for strategic reasoning -- for instance, Nash equilibria and many other solution concepts in game theory can be easily expressed -- which has an undecidable satisfiability problem and a non-elementary model checking problem. In this project, the aim is to study fragments of SL which can potentially have better results (decidability and complexitity) with respect to the satisfiability and model checking problems. The fragments to be studied can be either syntactic fragments of the full language or semantic fragments where only particular classes of models are considered.

Prerequisites: Discrete Mathematics, Introduction to Formal Proof, Logic and Proof

Desirable: Computer-Aided Formal Verification, Computational Complexity

Project type: theory

Building databases of mathematical objects in Sagemath (Python) Dmitrii Pasechnik

There is an enormous amount of information on constructing various sorts of ``interesting'', in one or another way, mathematical objects, e.g.

block designs, linear and non-linear codes, Hadamard matrices, elliptic curves, etc.  There is considerable interest in having this information available in computer-ready form.  However, usually the only  available form is a paper describing the construction, while no computer code (and often no detailed description of a possible implementation) is provided. This provides interesting algorithmic and software engineering challenges in creating verifiable implementations; properly structured and documented code, supplemented by unit tests, has to be provided, preferably in functional programming style (although  performance is important too).


Sagemath project aims in part to remedy this, by implementing such constructions, see e.g. Hadamard matrices in Sagemath: and


The project will contribute to such implementations.

There might be a possibility for participation in Google Summer of Code (GSoC) with Sagemath as a GSoC organisation, and being partially funded by the EU project ``Open Digital Research Environment Toolkit for the Advancement of Mathematics''

Prerequisites: Interest in open source software, some knowledge of Python, some maths background.

Building Heterogeneous Social Software, or, “How dare you tweet my snapchat?” Nigel Shadbolt, Max Van Kleek, Jun Zhao Social apps today require everybody to use the same application (e.g. Snapchat) or at least the same protocol (e.g. Twitter/Tweetdeck). This project explores how future social software could blur the boundaries between multiple social services by allowing the abstraction of social protocols for exchanging social information, while preserving the norms and social expectations around it. For example, Alice might send Bob a photo that should be deleted after its first viewing, and expect Bob to conform to that desire; to receive a ‘seen’ and ‘deleted’ receipt; and for Bob to be able to respond. To support this, we would require a novel language to express such social protocols and an architecture for allowing application designers to easily build complying social apps.
Privacy-Preserving Personal Information Environments Nigel Shadbolt, Max Van Kleek, Jun Zhao While the Internet of Things is likely to enable many significant new kinds of applications to make people’s lives easier, it also presents unprecedented threats to individual privacy, by introducing sensors into the most private locations and aspects of people’s lives. This project seeks to reverse current trends of having IoT-based sensors (ranging from environmental to wearable sensors) siphon data back to third party providers, by creating private Personal Information Environments for storing and managing sensor data under the individual’s control. The student will be involved in designing and implementing the foundational architecture for a decentralised, privacy-respecting Personal Information Environment.
Deciding satisfiability of formulas in the guarded negation fragment Michael Vanden Boom

The guarded negation fragment of first-order logic is an expressive logic of interest in databases and knowledge representation. It has been shown to have a decidable satisfiability problem but, to the best of my knowledge, there is no tool actually implementing a decision procedure for it.

The goal would be to design a tool to determine whether or not a formula in this logic is satisfiable. Most likely, this would require designing and implementing a tableau-based algorithm, in the spirit of related tools for description logics and the guarded fragment.

Prerequisites: Logic and Proof (or equivalent). There are some connections to material in Knowledge Representation and Reasoning, but this is not essential background

Interpolation Michael Vanden Boom

Let F1 and F2 be sentences (in first-order logic, say) such that F1 entails F2: that is, any model of F1 is also a model of F2. An interpolant is a sentence G such that F1 entails G, and G entails F2, but G only uses relations and functions that appear in *both* F1 and F2.

The goal in this project is to explore and implement procedures for constructing interpolants, particularly for certain decidable fragments of first-order logic. It turns out that finding interpolants like this has applications in some database query rewriting problems.

Prerequisites: Logic and Proof (or equivalent)

MSO Automata Michael Vanden Boom

The Automata, Logic, and Games course presents automata that run on infinite binary trees. However, in certain applications, it is natural to consider trees with unbounded or even infinite branching degree. The automata that run on trees like this are sometimes called MSO automata, since the transition function is described by a monadic second-order logic (MSO) formula, rather than by explicitly giving the state for each successor.

Although these MSO automata have been considered in the literature, the complexity of various operations on these automata is not well studied. The goal in this project is to fill this gap.

Prerequisites: Automata, Logic, and Games