Université de Rennes 1 Static analysis of numerical properties in the presence of pointers Analyse statique de propriétés numériques en présence de pointeurs Analyse statique Propriétés numérique Interprétation abstraite Analyse de pointeurs Must-aliasBisimulation Static analysis Numerical properties Abstract Interpretation Analysis of pointers Must-aliasBisimulation Logiciels‎ -- Vérification Thèses et écrits académiques Si la production de logiciel fiable est depuis longtemps la préoccupation d'ingénieurs, elle devient à ce jour une branche de sujets de recherche riche en applications, dont l'analyse statique. Ce travail a porté sur l'analyse statique de programmes et, plus précisément, sur l'analyse des propriétés numériques. Ces analyses sont traditionnellement basées sur le concept de domaine abstrait. Le problème est que, ce n'est pas évident d'étendre ces domaines dans le contexte de programmes avec pointeurs. Nous avons proposé une approche qui sait systématiquement combiner ces domaines avec l'information de l'analyse de points-to (une sorte d'analyse de pointeurs). L'approche est formalisée en théorie de l'interprétation abstraite, prouvée correct et prototypée avec une modular implémentation qui sait inférer des propriétés numériques des programmes de millions de lignes de codes. La deuxième partie de la thèse vise à améliorer la précision de l'analyse points-to. Nous avons découvert que l'analyse de must-alias (qui analyse si deux variables sont nécessairement égaux) peut servir à raffiner l'analyse points-to. Nous avons formalisé cette combinaison en s'appuyant sur la notion de bisimulation, bien connue en vérification de modèle ou théorie de jeu... Un algorithme de complexité quadruple est proposé et prouvé correct. The fast and furious pace of change in computing technology has become an article of faith for many. The reliability of computer-based systems cru- cially depends on the correctness of its computing. Can man, who created the computer, be capable of preventing machine-made misfortune? The theory of static analysis strives to achieve this ambition. The analysis of numerical properties of programs has been an essential research topic for static analysis. These kinds of properties are commonly modeled and handled by the concept of numerical abstract domains. Unfor- tunately, lifting these domains to heap-manipulating programs is not obvious. On the other hand, points-to analyses have been intensively studied to an- alyze pointer behaviors and some scale to very large programs but without inferring any numerical properties. We propose a framework based on the theory of abstract interpretation that is able to combine existing numerical domains and points-to analyses in a modular way. The static numerical anal- ysis is prototyped using the SOOT framework for pointer analyses and the PPL library for numerical domains. The implementation is able to analyze large Java program within several minutes. The second part of this thesis consists of a theoretical study of the com- bination of the points-to analysis with another pointer analysis providing information called must-alias. Two pointer variables must alias at some pro- gram control point if they hold equal reference whenever the control point is reached. We have developed an algorithm of quadruple complexity that sharpens points-to analysis using must-alias information. The algorithm is proved correct following a semantics-based formalization and the concept of bisimulation borrowed from the game theory, model checking etc. Electronic Thesis or DissertationText en application/pdf1 : 1017 Kohttp://ecm.univ-rennes1.fr/nuxeo/site/esupversions/25a42ce8-51ea-40ee-856e-4a41e8d51699 Fu Zhoulai 1983-01-02 CN 174164858 zhoulai.fu@gmail.com 2013REN1S060 http://www.theses.fr/2013REN1S060 2013-07-22 Informatique Université de Rennes 1thesis.degree.grantor_1 02778715X Université européenne de Bretagnethesis.degree.grantor_2 139075119 Université Rennes 1thesis.degree.grantor_3 Doctorat non ouiJensenThomasintervenant_1059884959PichardieDavidintervenant_2093668392 Mathématiques, informatique, signal, électronique et télécommunicationsecoleDoctorale_1 139007164 ddc:004 JensenThomasPichardieDavidUniversité de Rennes 1Sciences et technologie, médecine, pharmacie, odontologie, droit, économie, gestion, philosophieUniversité européenne de BretagnePôle de recherche et d'enseignement supérieur de BretagneUniversité Rennes 1Mathématiques, informatique, signal, électronique et télécommunicationsÉcole doctorale Mathématiques, informatique, signal, électronique et télécommunications (Rennes) ASCII PDF 1041462