Formal Methods
Formal methods use logic and mathematics to model, specify and verify systems, giving rigorous evidence about correctness, performance and reliability. At Glasgow we advance theory and tools and apply them to real software, networks and cyber‑physical platforms, including safety‑critical, autonomous and AI‑enabled systems. Our work covers probabilistic and real‑time model checking, game‑theoretic verification and synthesis, session and behavioural types for safe communication, logics for specification, and bigraph‑based models that capture structure, location, and connectivity, and their changes over time.
We develop and maintain widely used open‑source tools. PRISM enables quantitative verification of systems with randomness or uncertainty and has been recognised with long‑term impact awards. PRISM‑games extends this to stochastic multi‑player games, supporting concurrency and equilibria. BigraphER supports modelling, simulation and analysis of bigraph systems.
Applications span telecommunications and web services, sensor and IoT infrastructures, transport and digital twins, computational biology, security protocols, and safety assessments. We collaborate with engineering, life sciences, industry, and the public sector to ensure that methods scale to realistic designs and deliver trustworthy automation.
Project Highlights
TransiT
The TransiT project is focused on building an interconnected digital twin network that spans the whole transport system, including road, rail, maritime and aviation – across both passenger and freight.
PROBabLE Futures
Working alongside our law enforcement, third sector and commercial partners, the PROBable Futures project is developing a framework to understand the implications of uncertainty and to build confidence in future Probabilistic AI in law enforcement, with the interests of justice and responsibility at its heart.
PRISM Model Checker
PRISM is a probabilistic model checker, a tool for formal modelling and analysis of systems that exhibit random or probabilistic behaviour. It has been used to analyse systems from many different application domains, including communication and multimedia protocols, randomised distributed algorithms, security protocols, biological systems and many others.