M2 Pro - Méthodes de Vérification Formelle - 2014
Les supports de cours, ainsi que les corrigés des TDs sont disponibles
ici.
- Cours 1 sur les types de données abstraits et les fonctions récursives: Cours, TD corrigé et TD corrigé en Coq
- Cours 2 sur la logique pour la spécification de programmes: Cours et TD corrigé.
- Cours 3 sur la preuve inductive de programmes: Cours, TD et TD corrigé. Le devoir à la maison optionel peut compter pour le contrôle continu. La note finale pour la première partie du cours sera le maximum de ce devoir et de la première partie de l'examen final.
- Cours 4 sur la preuve de programmes impératifs en logique de Hoare: Cours, TD et corrigé.
- Cours 5 sur les preuves de terminaison de programmes impératifs en logique de Hoare: Cours et TD
