Gilles Barthe, Juan Manuel Crespo and César Kunz, who were part of the first generation of researchers at IMDEA Software, received the FME Lucas Award for their paper “Relational Verification Using Product Programs”, written during their time at the center.
The paper focuses on relational reasoning, a method used to verify two things: that the same program behaves similarly in two different runs, or that two different programs execute in a related fashion. This allows for the analysis of simulation and observational equivalence in programs, as well as properties such as continuity and non-interference.
Years after its publication, the impact of this work is still strongly perceived both inside and outside the formal methods community. In fact, its ideas and techniques are applied today in fields as diverse as software cost analysis, robustness in neural networks, or the security of smart contracts, among others.
From IMDEA Software, we would like to congratulate them on this well-deserved recognition, which rewards a long-term scientific work with a profound impact on modern computer science.
