Analyse Statique de Programmes Numériques: Ensembles Affines Contraints

We aim at proving automatically the correctness of numerical behavior of a program by inferring invariants on numerical variables. More precisely, we over-approximate in a sound manner the set of reached values. We use Abstract Interpretation-based Static Analysis as a generic framework to de ne and ap- proximate the semantics of a program in a uni ed manner. The semantics that describe the real behavior of the program (concrete semantics) is in general unde- cidable. Abstract interpretation o ers a way to abstract this concrete semantics to obtain a decidable semantics involving machine-expressible objects. We in- troduce a new affine forms-based abstract domain, called constrained affine sets, which extends and generalizes an already existing abstract domain introduced by Eric Goubault and Sylvie Putot. The expressiveness of such new domain is enhanced thanks to its ability to encode and propagate linear constraints among variables. We have implemented our new domain to experiment the precision and the efficiency of our approach and compare our results to the already existing abstract domains. The theoretical work as well as the implementation and the experiments have been the subject of two publications [CAV 2009, CAV 2010].Nous nous plaçons dans le cadre de l'analyse statique de programmes, et nous nous intéressons aux propriétés numériques, c'est a dire celles qui concernent les valeurs numériques des variables de programmes. Nous essayons en particulier de déterminer une sur-approximation garantie de l'ensemble de valeurs possibles pour chaque variable numérique utilisée dans le programme à analyser. Cette analyse statique est faite dans le cadre de la théorie de l'interprétation abstraite, théorie présentant un compromis entre les limites théoriques d'indécidabilite et de calculabilite et la précision des résultats obtenus. Nous sommes partis des travaux d'Eric Goubault et Sylvie Putot, que nous avons étendus et généralisés. Notre nouveau domaine abstrait, appelé ensembles affines contraints, combine à la fois l'efficacite de calcul des domaines à base de formes affines et le pouvoir ex- pressif des domaines relationnels classiques tels que les octogones ou les polyèdres. Le nouveau domaine a été implémenté pour mettre en évidence l'intérêt de cette combinaison, ses avantages, ses performances et ses limites par rapport aux autres domaines numériques déjà existants. Le formalisme ainsi que les résultats pra- tiques ont fait l'objet de plusieurs publications [CAV 2009, CAV 2010]