Vérification logicielle M2

Un panorama des méthodes formelles

8 exposés maximum, 20 minutes par exposé, l'ensemble des exposés doit tenir en moins de 2h45
Chaque exposé porte sur un thème distinct
Choisir un ou plusieurs articles ou un thème parmi ceux proposés ci dessous (liste non exhaustive) ou un développement Coq et transmettre ces infos aux délégués de promo qui s'assurent qu'un même sujet n'est pas sélectionné deux fois
Rédiger un résumé en français d'une quinzaine de diapos si possible en style Beamer de LaTeX et me transmettre le PDF par email au plus tard le 23 novembre 2023 23h59 (pénalités pour les retards)
S'assurer de la connexion avec le système de vidéo projection
Présenter ce résumé en français durant la séance du 27 novembre 2023

Un ou plusieurs articles de ce répertoire
Frama-C, voir ici ou là
Une des publications de Rustan Leino à propos de Dafny
Une librairie ou un module Coq, par exemple theories, Coq Package Index ou coq-contribs
Un document, un projet, une technique en lien avec le thème de ce module

En contrôle continu lors de la dernière séance de cours : exposés suivi d'un contrôle écrit. Le contrôle peut comporter des questions sur les exposés, des questions sur le cours et des exercices.
- N1 : exposé oral + diapos PDF, note/20
- N2 : contrôle écrit d'environ une heure sans document, note/20
- Note 1ère chance := (N1+N2)/2
- Note 2ème chance := N2
- Note finale pour tous := max(Note 1ère chance, Note 2ème chance)
Pour les M2 info, l'ensemble compte pour 50% du module IMC, soit 3 ECTS sur 6
Pour les M2 maths, l'ensemble compte pour l'intégralité des 3 ECTS du module
Pas de seconde session