Séminaire de l'Institut Thématique Interdisciplinaire (ITI) IRMIA++

La prochaine séance du séminaire de l'Institut Thématique Interdisciplinaire (ITI) IRMIA++ aura lieu ce jeudi 21 septembre mai à 9h, dans la salle de conférences IRMA.

Orateur : Arthur Charguéraud (ICube).

Titre : Interactive Program Verification

Résumé : Formal Verification enables one to prove that a program does not contain any bug. In this talk, I will present state-of-the-art techniques for formally verifying the implementation of a nontrivial algorithm or data structure. First, I will explain how to formulate as a mathematical theorem a statement of the form: "this program behaves as intended". Second, I will explain how to leverage an "interactive proof assistant", a tool for developing machine-checked mathematical proofs, for reasoning about the behavior of the source code of the program. Finally, I will give a survey of complex programs that have been formally verified in the past decade, assessing the progress made since the pioneering work by Hoare-Floyd-Dijkstra in the late 60's.