Optimisation et jeux appliqués à l'analyse statique de programmes par interprétation abstraite
L'interprétation abstraite est une méthode générale qui permet de déterminer de manière automatique des invariants de programmes. Cette méthode conduit à résoudre un problème de point fixe non linéaire de grande taille mais qui possède des propriétés de monotonie. Ainsi, déterminer des bornes s...
| Main Author: | |
|---|---|
| Language: | FRE |
| Published: |
Ecole Polytechnique X
2011
|
| Subjects: | |
| Online Access: | http://pastel.archives-ouvertes.fr/pastel-00607076 http://pastel.archives-ouvertes.fr/docs/00/65/10/43/PDF/these.pdf |
| Summary: | L'interprétation abstraite est une méthode générale qui permet de déterminer de manière automatique des invariants de programmes. Cette méthode conduit à résoudre un problème de point fixe non linéaire de grande taille mais qui possède des propriétés de monotonie. Ainsi, déterminer des bornes sur les valeurs prises par une variable au cours de l'exécution d'un programme, est un problème de point fixe équivalent à un problème de jeu à deux joueurs, à somme nulle et avec options d'arrêt. Cette dernière observation explique la mise en oeuvre d'algorithmes d'itérations sur les politiques. Dans un premier temps, nous avons généralisé les domaines numériques polyédriques par un domaine numérique abstrait permettant de représenter des invariants non-linéaires. Nous avons défini une fonction sémantique abstraite sur ce domaine à partir d'une correspondance de Galois. Cependant, l'évaluation de celle-ci est aussi difficile qu'un problème d'optimisation globale non-convexe. Cela nous a amené à définir une fonction sémantique relâchée, construite à partir de la théorie de la dualité, qui sur-approxime de la fonction sémantique abstraite. La théorie de la dualité a également motivé une construction d'une itération sur les politiques dynamique pour calculer des invariants numériques. En pratique pour des programmes écrits en arithmétique affine, nous avons combiné la relaxation de Shor et l'information des fonctions de Lyapunov quadratique pour évaluer la fonction sémantique relâchée et ainsi générer des invariants numériques sous forme d'ellipsoïdes tronquées. Le deuxième travail concerne l'itération sur les politiques et le calcul du plus petit point fixe qui fournit l'invariant le plus précis. Nous avons raffiné l'itération sur les politiques afin de produire le plus petit point fixe dans le cas des jeux stochastiques. Ce raffinement repose sur des techniques de théorie de Perron-Frobenius non-linéaire. En effet, la fonction sémantique abstraite sur les intervalles peut être vue comme un opérateur de Shapley en information parfaite: elle est semidifférentiable. L'approche conjointe de la semidifférentielle et des rayons spectraux non linéaires nous a permis, dans le cas des contractions au sens large de caractériser le plus petit point fixe. Cette approche mène à un critère d'arrêt pour l'itération sur politique dans le cas des fonctions affines par morceaux contractantes au sens large. Quand le point fixe est non minimal, le problème consiste à exhiber un point fixe négatif non nul de la semidifférentielle. Ce vecteur conduit à une nouvelle politique qui fournit un point fixe strictement plus petit que le point fixe courant. Cette approche a été appliquée à quelques exemples de jeux stochastiques à paiements positifs et de vérification de programmes. |
|---|