Thèmes des exposés
  Partie LM
  Partie MP
  1. Sémantique des programmes impératifs sous forme de système de transition étendus (STE)
    Défintion d'un compilateur traduisant des programmes impératifs en STE (sujet)

    Approfondissement: le compilateur en quelques lignes d'ocaml (programme à compléter)

  2. Recherche d'invariant et preuve de programme par calcul de plus faible précondition
    Application à la preuve de correction d'un algorithme d'exponentiation rapide (sujet, corrigé)

    Approfondissement: preuve de correction partielle d'un algorithme de recherche par dichotomie (preuve à compléter)

  3. Recherche d'invariant par interprétation abstraite : domaine des intervalles
    Application du calcul automatique des valeurs min et max des variables du programme suivant:
    prog(int j){ i:=100;
                 while(j>=10) do 
                   i:=i+1;
                   if (j<=i) then i:=i-1; j:=j-2; fi
                 od }
    
    (programme de l'analyseur, en ocaml, à compléter)
  4. Composition asynchrone et preuve d'invariants
    Application à la preuve de correction du protocol d'exclusion mutuelle du boulanger (bakery protocol)
    par la méthode de Floyd-Hoare
  5. Vérification par exploration exhaustive d'un graphe de comportement fini (model-checking)
    Application à la preuve de correction du protocol d'exclusion mutuelle de Burns
    en utilisant les opérateurs pre, post, wlp
  6. Vérification par abstraction et model-checking
    Application à la preuve de correction du protocol d'exclusion mutuelle du boulanger
    utilisation d'une abstraction pour se ramener à un graphe de comportement fini
Responsables IP : Laurent MOUNIER, Michaël PÉRIN