Formal Methods Research Group

School of Computing Science, University of Glasgow

About


The Formal Methods research group is part of the FATA section, School of Computing Science at the University of Glasgow.

Our research covers a wide range of topics, including process calculi, semantic models and logics, verification techniques based on types and type systems, formulation of model checking algorithms, techniques for efficient and scalable analysis including abstraction and symmetry reduction, and developing game theoretic techniques. A fundamental aspect of our research is the application of formal methods to the modelling, verification and synthesis of complex software systems including autonomous systems such as UAVs, location-aware, event-based systems, communication-based and distributed systems, telecommunications services, biochemical networks and cell signalling, security protocols and safety-critical systems.

We are also one of the principal developers of the probabilistic model checker PRISM - the most widely-used software tool for verification of probabilistic systems.

Latest News


Current Members


Muffy Calder

Prof Muffy Calder

Professor

View profile »

Simon Gay

Prof Simon Gay

Professor

View profile »

Alice Miller

Prof Alice Miller

Professor

View profile »

Gethin Norman

Dr Gethin Norman

Senior Lecturer

View profile »

Oana Andrei

Dr Oana Andrei

Research Fellow / Proleptic Lecturer

View profile »

Ornela Dardha

Dr Ornela Dardha

Lecturer

View profile »

Michele Sevegnani

Dr Michele Sevegnani

Lecturer

View profile »

Blair Archibald

Dr Blair Archibald

Research Assistant

View profile »

Laura Voinea

Ms Laura Voinea

Research Student

View profile »

William Kavanagh

Mr William Kavanagh

Research Student

View profile »

Ivaylo Valkov

Mr Ivaylo Valkov

Research Student

View profile »

Past Members


Ruth Hoffmann, Ryan Kirwan, Yu Lu, Chris Unsworth, Christopher Power, Andrea Degasperi, Robin Donaldson, Shamim Ripon, Vladislav Vyshemirsky, Alastair F. Donaldson, Stefan Reiff-Marganiec, Carron Shankland

Research projects and funding awards

Current

  • BehAPI: Behavioural Application Program Interfaces, an EU RISE network (March 2018 - February 2022) - Simon Gay
  • Science of Sensor Systems Software, EPSRC Program Grant (January 2016 - December 2020) - Muffy Calder (PI)
  • Explainable Social Group Interactions using Probabilistic Model Checking, University of Glasgow John Robertson Bequest (2018 - 2019) - Oana Andrei
  • 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)

Past

Software

  • Gethin Norman is one of the principal developers of the probabilistic model checker PRISM -- a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour.
  • Michele Sevegnani is the developer of BigraphER (Bigraph Evaluator & Rewriting) -- an implementation of Robin Milner's Bigraphical Reactive System (BRS) with an extension to bigraph with sharing.