Axe “Confiance et sécurité numérique”, 14 janvier 2021

Map Unavailable

Date(s) - 14/01/2021
14 h 00 - 16 h 00


Le prochain séminaire du Cédric sera organisé par l’axe 3, “Confiance et sécurité numérique”. Il aura lieu le 14 janvier à 14h, en visio conférence.


Armaël Guéneau. How can we formally verify (using a proof assistant) that a program is not only functionally correct, but also has the right asymptotic complexity?

In this talk, I will present the work carried out during my PhD. I will first argue that the use of the big-O notation — which is
standard in the algorithms literature — is also desirable in the context of formal specifications. I will then present our methodology
for mechanizing the proof of an algorithms’ complexity at the same time as its correctness, making it possible to carry out robust and
modular proofs of amortized, asymptotic bounds. Finally, I will describe our most challenging case study, where we apply our
methodology to the verification of a state-of-the-art incremental cycle detection algorithm.

Bio: Armaël Guéneau a soutenu sa thèse dans l’équipe INRIA Gallium en 2019 et est maintenant en post-doc à la Aarhus University au
Danemark dans l’équipe “Logic and Semantics” et le projet “Center for Basic Research in Program Verification”. Ses thématiques de
recherche concernent la vérification des propriétés de programmes ainsi que de leur complexité.

Chaima Zammali, doctorante et ATER. Robust state estimation for switched systems: Application to fault detection

Chaima Zammali received the Engineering degree from Ecole Nationale d’Ingénieurs de Tunis in 2017, the Ph.D. degree from the Sorbonne University in 2020. Currently, she is a Temporary Lecturer and Research Assistant at the Conservatoire National des Arts et Métiers, Paris, France. Her current research interests include switched systems estimation, set-membership analysis and fault diagnosis.