=====  Pré-requis =====

  * M1 Informatique : Sémantique et spécifications algébriques
  * M1 Informatique : Ingénierie de la preuve


=====  Contenu =====

  * Critères de qualité d'un système logiciel et enjeux de la certification. Exemples avec les langages et ateliers VDM, Z, B, UML...
  * Certification assistée par ordinateur avec Coq. 
    * Compléments sur le langage, les tactiques et les librairies. 
    * Techniques de définition de types et stratégies de preuves. 
    * Pré et post-conditions, invariants, gestion des exceptions. 
    * Modules et généricité des descriptions. Traduction en Coq des spécifications écrites dans d'autres systèmes.
  * Construction et certification de bibliothèques de programmes.
    * Formulation du raffinement de représentations de données. 
    * Obligations de preuves. 
    * Certification de la correction d'une implantation. 
    * Passage à la programmation concrète dans les différents types de langages.

===== Objectifs : savoir-faire et compétences =====

  * Connaître les différentes techniques de spécification, preuve et vérification de logiciel
  * Spécifier de manière formelle les parties critiques des logiciels
  * Découvrir et énoncer les propriétés qu'elles doivent vérifier
  * Mettre en oeuvre un système d'assistance à la spécification et à la preuve
  * Maîtriser le processus de raffinement de spécifications jusqu'à l'obtention d'un programme correct


===== Références bibliographiques =====

  - J.-F. Monin, Undestanding Formal Methods, Springer, 2003
  - Y. Bertot and P. Casteran, Theorem Proving and Program Development - Coq'Art, Texts in TCS, An EATCS Series, Springer-Verlag, 2004
  - J.-R. Abrial, The B_Book - Assigning Programs to Meanings, Cambridge Univ. Press, 1996
  - J.-Y. Girard et al., Proofs and Types, In Cambridge Tracts in TCS, Cambridge Univ. Press, 1989
  - E. Gamma et al., Design Patterns, Thomson Publishing, 1996

===== Notes de Cours =====

  * lien vers les slides
  * [[coq_2|Rappels]]