Gilles Barthe, Juan Manuel Crespo y César Kunz, quienes conformaron la primera generación de investigadores de IMDEA Software, recibieron el premio FME Lucas por su artículo “Relational Verification Using Product Programs”, escrito durante su etapa en el centro.
El artículo se centra en el razonamiento relacional, un método que sirve para comprobar dos cosas: que un mismo programa funciona de forma parecida en dos ejecuciones distintas, o que dos programas diferentes se ejecutan de manera relacionada. Esto permite analizar la simulación y la equivalencia observacional de los programas, así como propiedades como la continuidad y la no interferencia.
Años después de su publicación, el impacto de este trabajo se sigue percibiendo con fuerza tanto dentro como fuera de la comunidad de métodos formales. De hecho, sus ideas y técnicas se aplican hoy en campos tan diversos como el análisis de costes de software, la robustez en redes neuronales o la seguridad de los smart contracts, entre otros.
Desde IMDEA Software queremos darles la enhorabuena por este merecido reconocimiento, que premia un trabajo científico de largo recorrido en la informática actual.
