Michele Sevegnani

I am a Reader at the School of Computing Science, University of Glasgow. I obtained a PhD from the same institution for my work on bigraphs with sharing, a universal computational model that captures both spatial structure and dynamic behaviour. My thesis and other publications are in the Papers section.

My main research interest is the theory of bigraphs and how it can be used to reason about the safety, reliability and predictability of location-aware, event-driven systems, particularly when they are already deployed.

I am the lead developer of BigraphER, an open-source suite of tools for modelling, rewriting, simulating and visualising bigraphs.

My recent theoretical work focuses on the machine-checked formalisation of bigraphical algebra and rewriting semantics in Rocq, and on nondeterministic and sorted variants of bigraphs. I apply formal methods to digital twins for cyber-physical systems and human-autonomy teaming in connected vehicles. These methods now inform my work on future communication networks, complex transport systems and the responsible use of AI. Further details are available in the Research section.

I am involved in the following research projects:

• Co-lead of PROBabLE Futures (2024 - 2028) on the use of probabilistic AI in policing and the wider criminal justice and law enforcement system. This is a Keystone Project funded by Responsible AI UK.
• Investigator on TransiT (2024 - 2029), a national research hub to accelerate the decarbonisation of UK transport through digital twinning technologies. I lead a work package developing formal modelling and verification methods for federations of heterogeneous digital twins.
• Investigator on CHEDDAR (2024 - 2026), a national hub to advance future communications. My working group studies how formal verification can be used in the design of 5G and 6G protocols, including physical-layer security for integrated sensing and communication.

Earlier projects that I led include:

• British Council: The Alliance Hubert Curien Programme (2023 - 2025) on verified interaction with autonomous aircraft, in collaboration with ENAC, Toulouse (France).
• Amazon Research Award: Automated Reasoning (2022 - 2023) on diagrammatic formal modelling using bigraphs.
• FARM (2021 - 2023), a PETRAS project on formal methods for Agritech resilience.
• MAGIC (2020 - 2022), a PETRAS project on modelling perspectives in autonomous aerial and ground vehicles.

I have also secured funding for research on formal methods from the Royal Society, the Royal Society of Edinburgh, Taiwan's Ministry of Science and Technology and the London Mathematical Society. I was a visiting researcher at Cambridge and UC Berkeley.

Since 2025, I have been a member of the Editorial Board of Science of Computer Programming.

PhD opportunities

If you are interested in doing a PhD related to my research, please contact me. You can find information about the application process here.

I am currently recruiting PhD students on the following topics:

• Frugal and Verifiable User Interfaces for Autonomous Flight
  PhD project advertised through the MSCA COFUND BEST doctoral programme, based at ENAC and starting in September 2027. Applications close on 23 November 2026.

  The project uses bigraphs to analyse safety-critical user interfaces written in Smala. It will investigate which language features make verification expensive, how they can be simplified, and how to prove that these changes preserve the required safety properties.

  I will supervise the project with Cyril Allignol and Célia Picard at ENAC. The successful applicant will be based in Toulouse and spend the second year with my research group at the University of Glasgow, working on BigraphER and bigraphical semantics.

  Applicants should have a background in formal methods, verification, mathematical logic or programming languages. Experience with functional programming, preferably OCaml, would be useful but is not required.

  Applications are assessed through the BEST selection process. Applicants must also satisfy the programme's academic eligibility and MSCA mobility requirements. Apply here.

• Responsible Use of LLM-Based Tools in High-Stakes Decision-Making
  Fully funded position (covering home-level tuition fees and a stipend) for 42 months

  Large language models are increasingly considered for tasks in policing and criminal justice, including policy retrieval, intelligence summarisation, transcription, translation and form filling. Their use in these settings raises difficult questions about reliability, accountability and the evidential status of generated text. This project will address these questions and develop methods for assessing when, and under what safeguards, LLM-based tools can be used responsibly.

• Certified Verification of Post-Quantum Cryptographic Protocols

  Post-quantum protocols need assurance at several levels: the symbolic structure of the protocol, its cryptographic assumptions and its implementation. This project will investigate how symbolic verification, computational proofs and verified implementations can be connected in a single workflow. The student will use proof assistants and protocol-verification tools to establish security properties under explicit assumptions, while keeping the trusted computing base as small as practicable.

Teaching

• ADS2 — Algorithms and Data Structures 2 (second-year undergraduate)
  Course Coordinator. Introduction to the design and analysis of algorithms, covering sorting, searching, graph algorithms and complexity.
• PL — Programming Languages (Honours-level undergraduate)
  Foundations of programming language design, including operational semantics, type systems and implementation techniques.
• MRS — Modelling Reactive Systems (Honours-level undergraduate)
  Formal methods for specifying, verifying and analysing reactive and concurrent systems using process algebras and model checking.

Team

Postdoctoral researchers

• Ricardo Almeida (TransiT project)
• Susmoy Das (TransiT project)
• Grace Nyugoto (TransiT project)
• Evdoxia Taka (PROBabLE Futures project)

PhD students

• Austin Jon Dibble
• Duncan Guthrie
• Roberto Scott Luciani (SOCIAL AI CDT)

Former PhD students

• Maram Albalwe
  Thesis: Timed Bigraphs for Formal Verification of Sensor Network Routing Protocols
• Ebtihal Althubiti
  Thesis: Formalising privacy regulations with bigraphs
• Kyle Burns (co-supervised with Ciaran McCreesh)
  Thesis: Efficient and Scalable Algorithms for Bigraph Matching
• Surasak Phetmanee (co-supervised with Oana Andrei)
  Thesis: Rational verification for Stackelberg Security Games
• Xin Xin (co-supervised with Sye Loong Keoh)
  Thesis: Formal verification of safety-critical systems with uncertainty for Industry 4.0 applications

Former postdoctoral researchers

Yue Gu and Sana Hafeez (CHEDDAR project), Yining Hua and Abdul Raouf (Impact Acceleration Account) and Mengwei Xu (MAGIC project).

Former interns

Hassan Chamass, Sam Lynch, Cécile Marcon, Gabriel Nakach, Nicolas Nalpon, Thibault Rivoalen and Tianxiong Zhang.