A common theme in program verification is establishing relationships between two runs of the same program or of different programs. Such relationships can be proved by semantical means, or with syntactic methods such as relational program logics and product constructions. Gilles shall present an overview of these methods and their applications to provable security, differential privacy, and secure implementations.
Gilles Barthe is a research professor at the IMDEA Software Institute. His research interests include logic, formal verification, programming languages, and security. His current work focuses on verification and synthesis methods for cryptography and differential privac