The FME Lucas Award goes to Gilles Barthe, Juan Manuel Crespo and Cesar Kunz for their paper
published at the 17th International Symposium on Formal Methods (FM 2011).
Gilles Barthe receives the Lucas Award
The FME Awards Committee motivated its decision as follows:
This is a paper whose impact is perceived inside and outside our community. This includes, for example: deductive verification, invariant synthesis, neural networks, map-reduce program synthesis, cost analysis, and smart contracts. The paper is concerned with relational reasoning, as a means to establish that the same program behaves similarly on two diļ¬erent runs, or that two programs execute in a related fashion. This covers notions of simulation and observational equivalence, and properties such as non-interference and continuity. This paper shows how to reduce a proof of a relation between properties of two programs to a Hoare- style proof of a new property of a single (product) program. Several case studies are presented and the work is backed by the use of tools.
The paper is available here.