|
Evènement pour le groupe Modélisation et Verification
Date | 2009-04-30 11:00-12:15 |
Titre | Algorithmes 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é. |
Lieu | Salle 076, LaBRI, Rez-de-chaussée |
Orateur | Stéphane Gaubert |
Email | Stephane.Gaubert@inria.fr |
Url | INRIA and CMAP, Ecole Polytechnique |
Aucun document lié à cet événement. RetourRetour à l'index
| |