Cerca nel sito
ICube   >   Agenda : Séminaire de l'Institut Thématique Interdisciplinaire (ITI) IRMIA++

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

21 settembre 2023
Salle de conférences IRMA

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.

A propos de l'orateur :

Arthur Charguéraud is an Inria researcher, member of the ICube lab since 2016. He completed his PhD in 2010 at Inria Paris-Rocquencourt, then spent 18 months as a post-doc at the Max Plank Institute for Software Systems in Kaiserslautern. He was recruited at Inria Saclay in 2012, then moved to Strasbourg in 2016. His research is focused on program verification and program optimization.

Prochaine séance : le jeudi 19 octobre 2023 à 9h00.

À la une

Le dépôt des candidatures pour les postes d’enseignants-chercheur est ouvert. Les offres sont...

Flux RSS

Flux RSS