B53, room 4025
Speaker: Charles Grellois, Lecturer in Verification, University of Sheffield
Title: A journey in mathematical modeling, from program verification to new perspectives on digital twins
Abstract:
This talk will focus on the high level ideas and concepts, but further discussion on technical details is welcome.
I started working from my Masters’ years (2009-) on the verification of functional programs. We use mathematical techniques and tools to describe functional programs in a modular way, that is, the behaviour of a system must be obtained from the behaviour of its subcomponents. We have a property we want to verify over a program, and for that we model each subcomponent of this program in a way that reflects how it contributes to a tentative proof of that property.
The models at play come from elaborate algebra – category theory. However, the framework is such that we can see them as boxes that we wire together, just as we would with electronic components and boxes; and through the wires flow logical formulas, transformed by the components. The goal, in the end, is to get as output of the circuit the whole formula we want to check over the system. The big challenge lies in recursion – loops in the circuit.
After a high-level introduction to this, I will shift to current considerations of mine, that could be summed up as follows: we have designed great techniques and tools to model and analyse programs, but actually they apply to models of many more concrete situations! In a sense, we have reached a stage at which we can provide automated analysis of numerous discrete dynamical systems. Interestingly enough, model checking techniques brought to a different setting can for instance lead to in silico discoveries in life sciences, for instance.
I will also explain how one could look for automatic synthesis of “close” digital twins of systems described as sets of inputs and outputs. It is desirable to automatically generate models that are as close as possible to such “black boxes”, so as to be able to analyse them, or to verify them. In my idea, the class of models chosen for this automatic generation of “close digital twin” should be chosen so as to help either explainability or model-checking (that, as I will stress, can also be used to discover dynamic properties of the model in silico).
Bio:
Charles studied mathematics and theoretical computer science at Ecole Normale Supérieure de Cachan. He obtained his PhD from Université Paris Diderot in 2016, on the application of mathematical modeling to functional programs so as to verify their behaviour. He was a postdoctoral researcher in Bologna, on termination analysis of probabilistic functional programs, and then a Maître de Conférences (Lecturer) in Aix/Marseille, and then in Bordeaux. He joined the University of Sheffield in 2023 as a Lecturer in Verification.
In addition to his work on mathematics and logic applied to computer science, Charles started working a couple of years ago on maths and AI applied to medicine, with a couple of projects in their development phase at the moment.