Evènement pour le groupe Modélisation et Verification


Date 2009-04-30  11:00-12:15
TitreAlgorithmes de théorie des jeux en analyse statique de programme 
RésuméNous ferons un tour d’horizon de résultats portant sur la correspondance entre les équations de point fixe rencontrées en analyse statique de programme par interprétation abstraite et celles qui apparaissent dans l’approche par programmation dynamique des jeux répétés à somme nulle. Cette correspondance permet en particulier d’appliquer des algorithmes de type itération sur les politiques afin de déterminer des invariants de nature numérique sur le programme analysé (par exemple des invariants polyédraux). Cependant, deux difficultés apparaissent. La première, très inhabituelle, est que les jeux considérés peuvent avoir un taux d’escompte négatif (l’ensemble des points fixes n’est plus alors nécessairement connexe). Une seconde difficulté est que l’algorithme d’itération sur les politiques le plus simple peut terminer avec un point fixe non minimal, alors que c’est le point fixe minimal qui fournit le meilleur invariant. Nous montrons cependant comment utiliser des techniques de théorie de Perron-Frobenius non-linéaire (rayons spectraux, calcul semi-différentiel) pour obtenir toujours le plus petit point fixe, à condition que le taux d’escompte ne soit pas négatif. Ces résultats sont issus d’une série de travaux avec Éric Goubault, Matthieu Martel, Sylvie Putot, Alexandru Costan, Ankur Taly, et Assale Adjé. 
LieuSalle 076, LaBRI, Rez-de-chaussée 
OrateurStéphane Gaubert 
EmailStephane.Gaubert@inria.fr 
UrlINRIA and CMAP, Ecole Polytechnique 



Aucun document lié à cet événement.

Retour
Retour à l'index