Partager cette page :

Vérification déductive de programmes avec l'outil Why3

le 21 octobre 2026

13h15

Campus de Beaulieu ISTIC Campus de Beaulieu Amphi P - bât. 12D

Intervention de Jean-Christophe Filliâtre, directeur de recherche CNRS au Laboratoire Méthodes Formelles (CNRS / Université Paris-Saclay / ENS Paris-Saclay / INRIA Saclay - Île-de-France), dans le cadre des séminaires du département Informatique.

/medias/photo/seminaire-di_1630676501273-jpg

Ce séminaire a pour objectif de présenter la vérification déductive. Dans cette approche, la correction d'un programme est réduite à un ensemble d'énoncés mathématiques, dont la validité est ensuite établie à l'aide d'outils de démonstration automatique ou interactive. Les principales idées et techniques derrière cette approche seront illustrées à l'aide de l'outil Why3 développé au Laboratoire Méthodes Formelles de Paris-Saclay.

Ce séminaire est obligatoire pour les 1re et 2e années du département informatique de l'ENS Rennes, ainsi que pour les élèves de L3 défi.
Thématique(s)
Formation, Recherche - Valorisation
Contact
Martin Quinson (martin.quinson@ens-rennes.fr)

Mise à jour le 15 octobre 2026