FATA video

An overview of the FATA Research Section from the section head Professor David Manlove. Videos for each of the three research groups can be found further down this page.  


The Formal Analysis, Theory and Algorithms section (FATA) is a large and very active research group in theoretical computer science, currently leading or contributing to research grants with a total value of £12.6M (as per EPSRC, 30 July 2020).

Our research develops and applies mathematics and logic to the design and analysis of algorithms and complex computational systems. We are especially interested in bringing the clarity and insight of formal theories to hard application problems of real practical significance.

Our theoretical research is internationally leading as evidenced by recent publications in high-quality journals and conference proceedings.  Much of this work is driven by practical applications, such as verifying autonomous vehicles, analysing the spread of disease in livestock and matching kidney donors to patients.  We are also involved in modelling of the COVID-19 pandemic as part of the Royal Society's RAMP initiative.

Many of our projects are collaborative, as the section aims to apply formal ideas to problems of genuine interest outside the formal community itself.  Collaboration involves, for example, life scientists and communication system designers, companies in the telecommunications, software and pharmaceutical sectors, as well as government organisations.

Within FATA, there are three main research areas/groups with focus on specific research topics:

  • Algorithms and Complexity: algorithms for matching problems, combinatorial search and optimization, constraint programming, graph algorithms, phase transition phenomena in combinatorial problems, string algorithms, computational complexity, parameterised algorithms, counting and enumeration algorithms
  • Programming Language Foundations: programming language semantics and type systems, session types for concurrent and distributed systems, process algebras, quantum computation
  • Formal Methods: modelling and analysis of complex and reactive systems, probabilistic model checking, process algebras, bigraphs, graph algorithms, game theory, computational biology, telecommunications software and protocol analysis

The FATA section is led by Professor David Manlove.

Section members

Group of researchers

Group photo, November 2022

Top row, left to right: Jose Rodríguez Bacallado, Gethin Nroman, Douglas Fraser, Ivaylo Valkov, Surasak Phetmanee

Second row from the top, left to right: Lewis Dyer, Fabrizio Augusto Mendoza Granada, William Pettersson, Christopher Chandler, Duncan Paul Attard, Simon Fowler

Second row from the bottom, left to right: Sofiat Olaosebikan, Carlijn Bogaardt, Shruthi Prusty, David Manlove, Peace Ayegba, Vikraman Choudhury, Ciaran McCreesh

Bottom row, left to right: Jayakrishnan Madathil, Alice Miller, Jess Enright, Oana Andrei, Matthew McIlree, Laura Larios-Jones

Missing from the group photo as of Nov 2022: Muffy Calder, Simon Gay, Ornela Dardha, Kitty Meeks, Michele Sevegnani, Blair Archibald, John Sylvester, Mengwei Xu, Yue Gue, Jan De Muijnck-Hughes, Kyle Burns, Samuel Hand, Ethan Kelly, Magdalena Latifa

Academic Staff with academic role and affiliations to research groups/themes:

Honorary Research Fellow:

Research Staff:

Research Students:


Some highlights of our work include:

Recent News

March 2023 Ciaran McCreesh (as local chair) and other members of FATA are organising the 39th British Colloquium for Theoretical Computer Science (BCTCS'23) on 3-4 April 2023 in Glasgow - an annual event for UK-based researchers in theoretical computer science.

March 2023 Congratulations to Dr Ornela Dardha, who has been awarded the inaugural ‘Science, She Says!’ award by the Italian Ministry of Foreign Affairs and International Cooperation (MAECI). The award recognises an outstanding young female scientist, not of Italian descent, who has remarkably contributed to the advancement of science and technology and has strong connections with the Italian scientific community. The award is given to candidates from five regions across the world, with Dr Dardha winning the Europe award.

Jan 2023 Two positions are available on the KidneyAlgo project in the School of Computing Science, University of Glasgow, for a postdoc position and a Research Software Engineer position. Closing date for applications is 31 January 2023.

December 2022 Congratulation to Dr Sofiat Olaosebikan who started her permanent position today as Lecturer in Algorithms and Complexity.

November 2022 Congratulations to Prof David Manlove on being awarded an EPSRC grant KidneyAlgo: New Algorithms for UK and International Kidney Exchange in collaboration with Prof D. Paulusma from University of Durham.

August 2022 The School of Computing Science is seeking to appoint a Lecturer / Senior Lecturer / Reader in Algorithms and Complexity. Contact Professor David Manlove for informal enquiries. More details are available at this page, with closing date 30 September 2022.

July 2022 Ornela Dardha and Michele Sevegnani have been promoted to Senior Lecturer positions (equivalent to Associate Professors) starting 1 August 2022.

19 July 2022 Michele Sevegnani and Blair Archibald received an Amazon Research Award (Fall 2021) for their project “From Whiteboards to Models: Diagrammatic Formal Modelling for Everyone”.

19 July 2022 Ornela Dardha together with her co-authors Elena Giachino and Davide Sangiorgi received this year PPDP 10 Year Most Influential Paper Award for their paper Session types revisited.

1 June 2022 Dr Blair Archibald is now a Lecturer affiliated with both GLASS and FATA research sections, as well as with the Programming Languages research theme.

12 May 2022 FATA research on Algorithms for Paired Kidney Donation has led to world-leading impact according to REF 2021. This work, led by David Manlove, has been possible thanks to many collaborators over the years, notably Péter Biró, Gregg O’Malley, William Pettersson, and James Trimble.

1 May 2022 Dr Simon Fowler is now a Lecturer with the FATA research section.

12 August 2021 Congratulations to Dr Ciaran McCreesh for being awarded the prestigious Royal Academy of Engineering Research Fellowship for five years starting on 1 October 2021. The title of his project is "Trustworthy constraint programming and optimisation".



Over the past 10 years:

Research-led teaching

We are offering courses in advanced elements of algorithmics, model checking, programming languages, theory of computation. We are always looking for enthusiastic young people who are interested in Level 4 or MSci projects or PhD theses. More details on PhD projects and funded opportunities can be found here and a list of examples of PhD topics here.


Seminar series

FATA seminars are usually held on Tuesdays from 1pm to 2pm; see the Events tab for more details. If you would like to give a talk, please contact the FATA seminar convenor Larios-Jones Laura.

Events this week

There are currently no events scheduled this week

Upcoming events

FATA Seminar: MSci Project Talks

Group: Formal Analysis, Theory and Algorithms (FATA)
Speaker: Sidhant Bhavnani, Cameron Martin, University of Glasgow
Date: 28 March, 2023
Time: 13:00 - 14:00
Location: Room 422, SAWB

Title: SmolPB: Trimming Pseudo-Boolean Proof Logs

Abstract: Veripb is a state-of-the-art proof checker based on the cutting planes proof system that has successfully verified proofs for SAT, CP and Subgraph Isomorphism solvers. However, the size of these proof logs can be prohibitively large, making it challenging to store, transfer, and verify them efficiently. In this presentation, we propose SmolPB, a proof log trimming utility that reduces the size of proof logs produced in the Veripb format.

SmolPB identifies and removes redundant constraints from the proof logs while preserving their logical eqivalence. We demonstrate the effectiveness of SmolPB on a set of benchmarks and show that it achieves significant compression ratios.

Title: Writing Proof Logs Faster

Abstract: As Constraint Solvers become more widely used in industry, the concept of proof logging has become more important, particularly where solvers are being used in safety critical areas. This is because proof logging generates a mathematical proof along side a given solution, which can then be externally validated to ensure correctness. The problem however, is that currently the slow-down seen when comparing proof logging to standard solving is very large. This means that many time critical applications of solvers may not currently be suited to proof logging as its inclusion would make them too slow for their given tasks. The purpose of this MSci project was to take a solver with proof logging capabilities and examine its design to identify ways in which we may hopefully reduce the runtime of the proof logging process. 

FATA Seminar: MSci Project Talks

Group: Formal Analysis, Theory and Algorithms (FATA)
Speaker: -
Date: 11 April, 2023
Time: 13:00 - 14:00
Location: Room 422, SAWB

Abstract TBC

FATA Seminar

Group: Formal Analysis, Theory and Algorithms (FATA)
Speaker: Mike Vollmer, Tori Vollmer, University of Kent
Date: 18 April, 2023
Time: 13:00 - 14:00
Location: Room 422, SAWB

Abstract TBC

FATA Seminar - Special Delivery: Programming with Mailbox Types

Group: Formal Analysis, Theory and Algorithms (FATA)
Speaker: Simon Fowler, University of Glasgow
Date: 25 April, 2023
Time: 13:00 - 14:00
Location: Room 422, SAWB

The asynchronous and unidirectional communication model supported by mailboxes is a key reason for the success of actor languages like Erlang and Elixir for implementing reliable and scalable distributed systems. While many actors may send messages to some actor, only the actor may (selectively) receive from its mailbox. Although actors eliminate many of the issues stemming from shared memory concurrency, they remain vulnerable to communication errors such as protocol violations and deadlocks.
Mailbox types are a novel behavioural type system for mailboxes first introduced for a process calculus by de'Liguoro and Padovani in 2018, which capture the contents of a mailbox as a commutative regular expression. Due to aliasing and nested evaluation contexts, moving from a process calculus to a programming language is challenging. This paper presents Pat, the first programming language design incorporating mailbox types, and describes an algorithmic type system. We make essential use of quasi-linear typing to tame some of the complexity introduced by aliasing. Our algorithmic type system is necessarily co-contextual, achieved through a novel use of backwards bidirectional typing, and we prove it sound and complete with respect to our declarative type system. We implement a prototype type checker, and use it to demonstrate the expressiveness of Pat on a factory automation case study and a series of examples from the Savina actor benchmark suite.
[joint work with Duncan Paul Attard, Franciszek Sowul, Simon J. Gay, and Phil Trinder]

FATA Seminar

Group: Formal Analysis, Theory and Algorithms (FATA)
Speaker: Gergely Csáji, Eötvös Loránd University, Budapest
Date: 16 May, 2023
Time: 13:00 - 14:00
Location: Room 422, SAWB

Abstract TBC

Past events