• Titre: "Itérations sur les politiques et analyse de programme"
• Laboratoire: Laboratoire Sûreté du Logiciel, Commissariat à l'Energie Atomique, Saclay et INRIA Rocquencourt, projet Métalau
• Lieu du stage: CEA Saclay et INRIA Rocquencourt
• Nom (et coordonnées) du responsable du suivi du stagiaire éventuel:
  
  Eric Goubault (goubault@aigle.saclay.cea.fr)
  DTSI/SLA, CEA/Saclay
  91191 Gif-sur-Yvette
  et Stéphane Gaubert (Stephane.Gaubert@inria.fr)
  Projet Métalau
  INRIA-Rocquencourt - Bâtiment 12 - Domaine de Voluceau
  BP 105 - 78153 Le Chesnay cedex
• Nom (et coordonnées) du responsable administratif
  
  Laurence Charbonnier
  LIST/DTSI, CEA/FAR
  92260 Fontenay-aux-Roses
  et
  Françoise Feneck
  BPAS, INRIA
  78153 Le Chesnay Cédex.
  
  
• Sujet
  
  Dans un analyseur statique, l'outil considère le programme comme une fonctionnelle sur une structure partiellement ordonnée (en général, un treillis complet, c'est à dire un ordre partiel qui admet les sups et les infs - comme c'est le cas pour les intervalles de valeurs), dont le plus petit point fixe donne par exemple des invariants du programme. Il est donc crucial d'avoir de bons algorithmes permettant de calculer rapidement et précisément ces points fixes (ou des sur-approximations).
  
  Des algorithmes rapides de type Newton, dits d'itération sur les politiques, on été développés récemment pour le calcul de points fixes de classes d'applications monotones dans Rⁿ, qui interviennent dans les problèmes de jeux à deux joueurs et somme nulle, et sont données par des expressions faisant intervenir les lois min,max, et plus.
  
  Dans un premier temps, on demandera au stagiaire de comprendre les concepts de base concernant l'itération sur les politiques. On pourra prendre comme premier exemple le treillis des intervalles sur les entiers (et toutes ses puissances finies). Afin de pouvoir appliquer ces nouveaux types d'algorithmes, il faudra savoir approximer les fonctionnelles produites par la sémantique des programmes par des fonctionnelles de type min-max-plus.
  
  Un deuxième aspect du stage sera d'essayer de généraliser ces résultats à des treillis d'analyse statique plus intéressants; par exemple le treillis des relations linéaires, celui des polyhèdres convexes, ou encore des octogones. On pourra expérimenter ces nouvelles idées en en implémentant certains aspects.
  
  
• Matériel utilisé: PC sous LINUX
• Connaissances préalables attendues chez le stagiaire: une aisance en informatique et en mathématiques appliquées.

This document was translated from L^AT_EX by H^EV^EA.