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

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.