Opimisation and games applied to static analysis by abstract interpretation
Optimisation et jeux appliqués à l'analyse statique de programmes par interprétation abstraite
Résumé
The abstract interpretation is a general method to compute automatically program invariants. This method leads to solve a non-linear fixed point equation involving a monotone function. Determining numerical invariants in order, for instance, to give bounds on the values taken by the variables of a program, turns out to be equivalent to solving a two-player zero-sum game with stopping options. This observation allows one to transport algorithms from game theory, like policy iteration, to abstract interpretation. The first contribution of this thesis is the generalisation of these abstract polyhedraic numerical domains. We construct a general abstract numerical domain which encompasses all the classical ones. We define an abstract semantic function in terms of a Galois connection. However, evaluating the abstract semantic function is as hard as solving a non-convex global optimization problem. Hence, we define a second semantic function called relaxed semantics constructed from duality theory, which provides a safe overapproximation of the abstract semantic function. The duality theory also motivates the construction of a dynamical policy iteration algorithm to compute numerical invariants. In practice for programs written in affine arithmetic, we combine Shor's relaxation scheme and Lyapunov functions to evaluate the relaxed semantic function and so generate numerical invariants which are the form of truncated ellipsoids. The second contribution concerns policy iteration and computation of the smallest fixed point problem which provides the more precise invariant. We refined the policy iteration algorithm in order to compute the smallest fixed point, in the case of stochastic games. The refinement is based on non-linear Perron-Frobenius theory. However, since the abstract semantic function in the case of interval domain can be interpreted as a Shapley operator in perfect information, we use a weaker notion of differentiability: it is semidifferentiable. The approach by the semiderivatives combined by non-linear spectral radius allows us to characterise the fixed points in the non-expansive case. In the case of non-expansive and piecewise affine (Shapley) operators, the characterisation leads to a termination criteria for policy iteration. When the fixed point found by policy iteration is not minimal, the problem is reduced to finding a non-positive fixed point for a semiderivative map. This vector provides a descent direction which leads to a new policy and then to a strictly smaller fixed point. This approach has also been applied to typical examples arising from game or program verification problems.
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.