Mathematical Modelling

All formal systems are underpinned by mathematical models.

Our experts study how to construct models for challenging targets such as advanced higher-order programming languages with a variety of effects or finding game and information-theoretic accounts for cybersecurity and how to characterise relations between different models of the same system.

Our researchers have been pivotal in developing such techniques as game semantics, modelling programs as a game between the code and its computational context, and have developed new forms of automata to model higher-order code, such as nominal and fresh-register automata. But they are not just concerned with building models, they also work on their validation. This approach emphasises the alignment between mathematical representations and real-world observations. Our researchers apply this rigorous approach to assess the correspondence between model assumptions and empirical data, particularly in the context of weak memory persistency models and RDMA semantics under TSO models.

By ensuring the coherence of these mathematical abstractions with practical scenarios, we strive to bolster the reliability and effectiveness of mathematical models across diverse applications.

Getting a model of SPIR-V (author: Vasileios Klimis, with permission)