Filière Programmes et preuves - DESS MINT - Faculté des sciences de Luminy

Responsable de la filière : Yves Lafont


Présentation de la filière

Les logiciels sont de plus en plus complexes et interdépendants. Pour assurer la cohérence et la correction des programmes ou des circuits, on devra inévitablement recourir aux méthodes formelles inspirées, entre autres, par la logique mathématique.


Cours de mise à niveau (25h) : Logique et calcul, par Marie-Renée Fleury-Donnadieu (Département de Mathématiques, Institut de Mathématiques de Luminy)

Notions sur les arbres - Calcul propositionnel - Calcul des prédicats - Déduction naturelle - Lambda-calcul pur et typé.


Tronc commun (25h) : Preuves, par Yves Lafont (Département de Mathématiques, Institut de Mathématiques de Luminy) et Antoine Rauzy (Institut de Mathématiques de Luminy)

Calcul des séquents - Preuves par récurrence - Démonstration assistée par ordinateur.

Examens : 2001 - 2002 - 2003.


Approfondissement et application (25h) : Vérification de modèles, par Antoine Rauzy (Institut de Mathématiques de Luminy)

Pour vérifier qu'un logiciel fait bien ce que l'on attend de lui, la méthode traditionnelle consiste à lui faire passer une série de tests. Cependant, cette méthode ne donne jamais la certitude que le logiciel fonctionne correctement, car les tests ne peuvent pas être exhaustifs (étudier tous les scenarii d'utilisation pour tous les jeux de données serait d'un coût prohibitif). Pour le logiciel classique, on s'accomode de cette incertitude. Pour les parties critiques des logiciels critiques (tels que ceux mis en oeuvre dans les avions), d'autres techniques sont employées :

L'option vise à présenter cette dernière technique. On étudiera en particulier : Des exemples pourront être traités avec le vérificateur de modèle SMV.


Bibliographie


Stages 2003

Trusted Logic (Sophia-Antipolis)