2 Cours en parallèle   (LM || MP)
  Partie LM
  Partie MP
  1. Preuve de programmes impératifs : technique de Dijkstra-Floyd-Hoare
  2. Recherche d'invariant par interprétation abstraite
  3. Vérification à l'aide des opérateurs : pre, post, wlp
  4. Construction de modèles finis par abstraction
Responsables IP : Laurent MOUNIER, Michaël PÉRIN