Cours Master Recherche Informatique
    Filière Modélisation et Vérification
Cours Master Professionnel Informatique (2ième année)
    Filière Fiabilité et Sûreté des Systèmes Informatiques

Programme du cours
Bibliographie
Travaux dirigés
__________________________________________________________________________________________

Module Méthodes formelles
Programme
__________________________________________________________________________________________
Bibliographie
                        Logique, réduction, résolution
.  René Lalement. Masson.
                        Le Coq'Art. Y. Bertot et P. Castéran. Springer-Verlag.
                        Circuit Certification in Type Theory,  S. Coupet-Grimal et L. Jakubiec.
                             Copyright : Springer-Verlag.
Formal Aspects of Computing  .
                              Vol 16 No 4, pp 352 - 373, Nov 2004.
                        An Axiomatization of Linear Temporal Logic in The Calculus of Inductive Constructions
                             
S. Coupet-Grimal. The Journal of Logic and Computation,
                              Vol 13 No  6, pp 801-813, 2003
                        Formal Verification of an Incremental Garbage Collector.
                             S. Coupet-Grimal, C.
Nouvet,  The Journal of Logic and Computation,
                             Vol 13 No  6, pp 815-833, 2003.
_____________________________________________________________________________________________

Travaux dirigés  

TD1 Apprentissage du Lambda-Calcul pur comme langage de programmation. ps, pdf 
TD2 Introduction au Lambda-Calcul simplement typé. ps, pdf
TD3 Autres principes de récurrence et arithmétique. ps, pdf
TD4 Définitons inductives et récursives,  prédicats odd et even, listes. ps, pdf
TD5  Certification en Coq d'un additionneur n-bits. ps, pdf.