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.
Overview
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 funded by a range of organisations, including EPSRC, Responsible AI UK, the Royal Academy of Engineering, and the Leverhulme Trust. We currently host three research fellowships.
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.
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: graph algorithms, counting and enumeration algorithms, parameterised algorithms, algorithmic game theory, algorithms for matching problems, constraint programming and algorithm engineering.
- 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.
- Programming Language Foundations: programming language semantics and type systems, session types for concurrent and distributed systems, process algebras, quantum computation.
The FATA section is led by Professor David Manlove.
Section members
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:
- Professor Dame Muffy Calder - Professor of Formal Methods, Vice Principal & Head of College of Science and Engineering - Formal Methods, Understandable Autonomous Systems
- Professor Simon Gay - Professor of Computing Science (Head of School) - Formal Methods, Programming Languages, Understandable Autonomous Systems
- Professor David Manlove - Professor of Algorithms and Complexity (FATA Section Head) - Algorithms and Complexity
- Professor Alice Miller - Professor of Computing Science - Formal Methods, Understandable Autonomous Systems
- Dr Jessica Enright - Reader - Algorithms and Complexity, Understandable Autonomous Systems
- Dr Kitty Meeks - Reader - Algorithms and Complexity
- Dr Ornela Dardha - Senior Lecturer - Formal Methods, Programming Languages, Understandable Autonomous Systems
- Dr Yiannis Giannakopoulos - Senior Lecturer - Algorithms and Complexity
- Dr Gethin Norman - Senior Lecturer (Deputy Head of School) - Formal Methods, Understandable Autonomous Systems
- Dr Michele Sevegnani - Senior Lecturer - Formal Methods
- Dr Oana Andrei - Lecturer - Formal Methods, Understandable Autonomous Systems, Centre for Computing Science Education
- Dr Blair Archibald - Lecturer - Systems, Formal Methods, Programming Languages
- Dr Simon Fowler - Lecturer - Programming Languages
- Dr Ciaran McCreesh - Research Fellow - Algorithms and Complexity, Understandable Autonomous Systems
- Dr Sofiat Olaosebikan - Lecturer - Algorithms and Complexity
- Mr Ivaylo Valkov - Lecturer - Formal Methods
Honorary Research Fellow/Lecturer:
Research Staff:
- Dr Ricardo Almeida
- Mr Duncan Paul Attard
- Dr Carlijn Bogaardt
- Dr Rachael Colley
- Dr Tom Davot
- Dr Arthur Gontier
- Dr Yue Gu
- Miss Sana Hafeez
- Mr Jayakrishnan Madathil
- Miss Danielle Marshall
- Dr William Pettersson
Research Students:
Highlights
Some highlights of our work include:
- Hosting the 39th British Colloquium for Theoretical Computer Science (BCTCS) in 2023.
- Hosting the 48th International Colloquium on Automata, Languages, and Programming (ICALP) in 2021.
- Developing algorithms for the UK Living Kidney Sharing Scheme, which have helped to identify over 1,900 kidney transplants.
- Involvement in three current/recent EPSRC programme grants (Populations, ABCD, S4).
- Leadership of two current/recent COST Actions (BETTY, ENCKEP).
- Dr Ciaran McCreesh's Research Fellowship from the Royal Academy of Engineering Research.
- Dr Kitty Meeks's Research Fellowship from the Royal Society of Edinburgh.
- Prof David Manlove’s award of the Royal Society of Edinburgh Lord Kelvin Medal.
- Prof Muffy Calder’s high-profile lectures, including the Strachey Lecture and the George Boole 200 Inaugural Lecture.
- Excellent outreach activities, including PWSA (Programming Workshop for Scientists in Africa) run by Dr Sofiat Olaosebikan.
Recent News
June 2024 Alice Miller has been awarded a research fellowship funded by the Leverhume Trust, with the project titled "Combinatorial solutions for maximum allocations".
April 2024 Gethin Norman has been awarded the 2024 ETAPS Test-of-Time Tool Award with his long-term collaborators Marta Kwiatkowska and Dave Parker from the University of Oxford for their probabilistic model checking tool PRISM. (Award ceremony photo)
March 2024 Yiannis Giannakopoulos has been appointed as Turing Fellow by the Alan Turing Institute.
August 2023 Matthew McIlree and Ciaran McCreesh received the best paper award at CP 2023 for their paper "Proof Logging for Smart Extensional Constraints".
August 2023 Ciaran McCreesh was awarded the Association for Constraint Programming (ACP) Early Career Researcher Award at the CP 2023 conference. (Award ceremony photo)
June 2023 Prof Alice Miller has been awarded an EPSRC grant M4Secure: Making Memory Management More Secure with Dr Jeremy Singer as PI.
June 2023 We are welcoming Dr Yiannis Giannakopoulos who joins the School of Computing Science as Senior Lecturer on 1 June 2023!
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 Dr Ornela Dardha 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 Dr Sofiat Olaosebikan started her permanent positionas Lecturer in Algorithms and Complexity.
November 2022 Prof David Manlove has been 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 Dr Ciaran McCreesh was 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".
Projects
Current (or shortly about to start):
- TransiT Hub (Twinning for Decarbonising Transport) (EPSRC, 2024 - 2029) - Co-Is: Prof Muffy Calder, Dr Michele Sevegnani, Dr Blair Archibald
- PROBabLE Futures (Probabilistic AI Systems in Law Enforcement Futures) (UKRI Responsible AI UK, 2024 - 2028) - Dr Michele Sevegnani(Co-Lead), Prof Muffy Calder (Co-I)
- SecureSense (CHEDDAR Hub, 2024 – 2025) - Dr Michele Sevegnani (Co-I)
- M4Secure: Making Memory Management More Secure (EPSRC, 2023 - 2026) - Prof Alice Miller (co-I)
- Uni-pi: safety, adaptability and resilience in distributed ecosystems, by construction (EPSRC, 2023 - 2026) – Dr Ornela Dardha (PI)
- KidneyAlgo: New Algorithms for UK and International Kidney Exchange (EPSRC, 2023 - 2025) - Prof David Manlove (PI)
- Multidisciplinary Ecosystem to study Lifecourse Determinants and Prevention of Early-onset Burdensome Multimorbidity (NIHR, 2022 - 2024) – Dr Jess Enright (co-I)
- Digitalisation of livestock data to improve veterinary public health (NordForsk, 2021 - 2024) – Dr Jess Enright (PI)
- Trustworthy Constraint Programming and Optimisation (RAEng, 2021 - 2026) – Dr Ciaran McCreesh (PI)
- Beyond One Solution in Combinatorial Optimisation (EPSRC, 2021 - 2026) - Dr Kitty Meeks (PI), Dr Jess Enright (Co-I)
- UKRI Trustworthy Autonomous Systems Node in Governance and Regulation (EPSRC, 2020 - 2024) - Prof Alice Miller (Co-I)
- Assurance and Resilience of Digital Twins in Critical Systems (EPSRC/DSTL Industrial Case Award, 2020 - 2025) - Prof Alice Miller (PI)
- Session Types for Reliable Distributed Systems (STARDUST) (EPSRC, 2020 - 2024) - Prof Simon Gay (PI), Dr Simon Fowler (co-I)
- Multilayer Algorithmics to Leverage Graph Structure (MultilayerALGS) (EPSRC, 2020 - 2025) - Dr Kitty Meeks (PI) and Dr Jess Enright (co-I)
Over the past 10 years:
- KEP-SOFT: Software for Transnational Kidney Exchange Programmes (COST, 2021-2022), Prof David Manlove (PI)
- Formal methods for Agritech Resilience Modelling (FARM) (PETRAS, 2021 - 2022) - Dr Michele Sevegnani (PI), Prof Muffy Calder (Co-I)
- Real-time monitoring and predictive modelling of the impact of human behaviour and vaccine characteristics on COVID-19 vaccination in Scotland (UKRI, Mar 2021 - Sep 2022) - Dr Jess Enright is co-Investigator
- Consent Verification in Autonomous Systems (UKRI Trustworthy Autonomous Systems Hub - Pump priming programme, July 2021 - June 2022) - Prof Alice Miller is co-Investigator, Dr Inah Omoronyia is the PI.
- Multi-Perspective Design of IoT Cybersecurity in Ground and Aerial Vehicles (MAGIC) (PETRAS, 2020 - 2021) - Dr Michele Sevegnani (PI), Prof Muffy Calder (co-I)
- Behavioural Application Program Interfaces (2018-2022) – Dr Ornela Dardha (UoG Site Leader), Prof Simon Gay
- IP-MATCH: Integer Programming for Large and Complex Matching Problems (2017 - 2020) - Dr David Manlove (PI)
- Modelling and Optimisation with Graphs (2017 - 2020) - Dr Patrick Prosser (PI), Dr Jess Enright (co-I), Dr Ciaran McCreesh (Researcher Co-I)
- European Network for Collaboration on Kidney Exchange Programmes (2016-2020) – Prof David Manlove (Chair)
- Science of Sensor Systems Software (2016 - 2022) - Prof Muffy Calder (PI)
- Exploiting Parallelism through Type Transformations for Hybrid Manycore Systems (2014 - 2020) - Prof Simon Gay (Co-I)
- From Data Types to Session Types: A Basis for Concurrency and Distribution (2013 - 2020) - Prof Simon Gay (PI), Dr Ornela Dardha (Co-I)
- Formal methods for Internet of Things (IoT) device management platforms - The Royal Society of Edinburgh, Joint Project with Ministry of Science and Technology Taiwan (MOST) (2017-2019) - Michele Sevegnani (PI)
- Collaboration Seeding, EPSRC Impact Acceleration account (June 2017-June 2019) - Alice Miller (PI)
- Explainable Social Group Interactions using Probabilistic Model Checking, University of Glasgow John Robertson Bequest (2018-2019) - Oana Andrei (PI)
- Glasgow Molecular Pathology Node (2015-2019) – Prof Muffy Calder (Co-I)
- EPSRC Institutional Sponsorship Fund project: "New algorithms for paired and altruistic kidney donation" (October 2015 - March 2016) - Dr David Manlove (PI)
- EPSRC Impact Acceleration Account - Algorithms for Paired and Altruistic Kidney Exchange (01/01/2015-30/09/2015) - Dr David Manlove
- A Population Approach to Ubicomp System Design (2011-2017) - Prof Muffy Calder (co-I)
- Efficient Algorithms for Mechanism Design Without Monetary Transfer (2013-2016) - Dr David Manlove (PI)
- COST Action IC1201: Behavioural Types for Reliable Large-Scale Software Systems (2012-2016) - Prof Simon Gay (Chair)
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.
Courses:
- COMPSCI4009 Algorithmics I (H)
- COMPSCI4003 Algorithmics II (H)
- COMPSCI5116 Computational Game Theory (M)
- COMPSCI5006 Constraint Programming (M)
- COMPSCI4031 Modelling Reactive Systems (H)
- COMPSCI5057 Modelling Reactive Systems (M)
- COMPSCI4016 Programming Languages (H)
- COMPSCI4105 Quantum Computing (H)
- COMPSCI4072 Theory of Computation (H)
Seminar series
FATA seminars are usually held on Tuesdays from 3pm to 4pm; see the Events tab for more details. If you would like to give a talk, please contact the FATA seminar convenor Jayakrishnan Madathil.
Events this week
There are currently no events scheduled this week
Upcoming events
[FATA Seminar] Bigraphs as a theoretical base for verifying interactive systems
Group: Formal Analysis, Theory and Algorithms (FATA)
Speaker: Cyril ALLIGNOL and Celia PICARD, Ecole Nationale de l'Aviation Civile
Date: 10 December, 2024
Time: 15:00 - 16:00
Location: Sir Alwyn Williams Building, 422 Seminar Room
Abstract: Interactive systems are multiplying, including in critical aeronautical systems such as aircraft cockpits and air traffic control systems. At the same time, UIDLs, the languages that enable the development of such systems, are also on the rise. However, to date, these languages offer no guarantees, neither in terms of compilation nor on the systems developed. Hence the need for a verified programming framework for UIDLs. This is the main subject of our research.
In this talk, we will present the results we have obtained so far and our ongoing work, namely: using bigraphs to express the semantics of UIDLs; defining a formal minimal UIDL based on bigraphs; formalising the bigraph theory in the Coq proof assistant. We will also discuss our future work around the verification of interactive systems, including the verification of interactive properties.
-----------------------------------
This event is part of the FATA Weekly Seminar, which takes place every Tuesday from 3:00 - 4:00 PM in Room 422, Sir Alwyn Williams Building and on Zoom https://uofglasgow.zoom.us/j/83611964233?pwd=CgRyzxK8Z9fP2ULTb5ONWZeUYx2t2E.1
[FATA Seminar] Formally verified hardening of C programs against fault injection
Group: Formal Analysis, Theory and Algorithms (FATA)
Speaker: Basile PESIN, Ecole Nationale de l'Aviation Civile
Date: 10 December, 2024
Time: 15:00 - 16:00
Location: Sir Alwyn Williams Building, 422 Seminar Room
Abstract: Fault attacks allow malicious actors to modify the behavior of a program by
physically injecting a fault in the hardware. They typically target sensitive
applications such as cryptography services, authentication or boot-loader and
firmware updater. They can be defended against by adding countermeasures, that
is control flow checks and redundancies, either in the hardware, or in the
software running on it. In particular, software countermeasures may be added
automatically during compilation.
In this talk, we will describe a formally verified implementation of this
approach in the CompCert verified compiler for the C language. We proposed a
toolkit to implement countermeasures as transformations of a middle-end
representation of CompCert, RTL. We applied this toolkit to two existing
countermeasures that protect the control flow of the program. We proved that
these countermeasures are correct, that is, they do not change the observable
behavior of the program during an execution without fault injection. We then
modeled the effect of a fault on the behavior of the program as an extension of
the semantic model of RTL. We used this new model to formally prove the efficacy
of the countermeasure: all attacks are caught. In addition to this formal
reasoning, we evaluated the protected program using Lazart, a tool for symbolic
fault injection.
-----------------------------------
This event is part of the FATA Weekly Seminar, which takes place every Tuesday from 3:00 - 4:00 PM in Room 422, Sir Alwyn Williams Building and on Zoom https://uofglasgow.zoom.us/j/83611964233?pwd=CgRyzxK8Z9fP2ULTb5ONWZeUYx2t2E.1
Past events
Research Groups in FATA
Algorithms and Complexity
An overview video of the research activities carried out by the members of this group can be found at this youtube link.
Formal Methods
An overview video of the research activities carried out by the members of this group can be found at this youtube link.
Programming Languages
An overview video of the research activities carried out by the members of this group can be found at this youtube link.