About
The pervasive adoption of distributed software systems in our society is drastically changing the landscape of the global digital infrastructure and economy. To avoid catastrophe, it is imperative that these systems behave as intended, even under constantly changing environmental conditions, software upgrades, or unplanned events, such as failures or service degradation. This project aims to develop Uni-pi, the first unified formal model based on the pi-calculus and linear/session types for the verification of safety, adaptability and resilience properties, whilst maintaining a realistic view of distributed software ecosystems in the presence of failures, message inconsistencies or service degradation.
Safety
The guarantee that software behaves as intended, with an absence of unexpected or unaccounted-for communication.
Adaptability
The ability for software to safely update its intended behaviour at runtime, i.e., post-deployment.
Resilience
The capability of software to provide intended outputs in spite of a degree of failures occurring at runtime.
Uni-pi will be fully mechanised to obtain a correct-by-construction meta-theory.
Uni-pi will be evaluated against practices and case studies from industry, by working closely with our industrial partners Actyx and SingularityNET. This project will lay the foundations for a new generation of mainstream programming languages, software tools and distributed ecosystems of the future that are safe, adaptable, and resilient, by construction.
Uni-pi is funded by EPSRC, grant number EP/X027309/1.
People
Organisations
Lead Research Organisation
Project Partner
Project Partner
Publications
Proceedings Papers
- Multiparty Session Types with a Bang!
-
Matthew Alan Le Brun, Simon Fowler, Ornela Dardha
European Symposium on Programming (ESOP) 2025 - MAGĻ!: The Role of Replication in Typing Failure-Prone Communication
-
Matthew Alan Le Brun, Ornela Dardha
Formal Techniques for Distributed Objects, Components, and Systems (FORTE) 2024 - Coconut: Typestates for Embedded Systems
-
Arwa Hameed Alsubhi, Ornela Dardha
Coordination Models and Languages (COORDINATION) 2024
Journal Papers
- Design and Evaluation of Coconut: Typestates for C++
-
Arwa Hameed Alsubhi, Ornela Dardha, Simon J. Gay
Science of Computer Programming 2025