Algèbres de Kleene pour l'analyse statique des programmes : un nouveau cadre

L'analyse statique des programmes consiste en un ensemble de techniques permettant de déterminer des propriétés des programmes sans avoir à les exécuter. Parmi les applications de l'analyse statique des programmes, nous retrouvons l'optimisation du code source par des compilateurs et la détection de code malveillant ou de code qui pourrait être exploité à des fins malveillantes. L'évidente pertinence et l'importance (parfois critique) de telles applications expliquent les nombreuses tentatives de compréhension du cadre théorique général de l'analyse statique des programmes. Les algèbres de Kleene sont la théorie algébrique des automates finis et des expressions régulières. Cet outil algébrique s'est avéré très approprié pour l'analyse statique et la vérification des programmes. Le but de cette thèse est de développer un cadre algébrique basé sur les algèbres de Kleene pour calculer les solutions d'une classe générale de problèmes intraprocéduraux d'analyse de flot de données. Ce cadre permet de représenter les programmes, ainsi que leurs propriétés, d'une manière homogène, compacte et expressive. Les algorithmes traditionnels employés pour calculer le résultat d'une analyse sont alors remplacés par des manipulations algébriques des éléments d'une algèbre de Kleene.Static program analysis consists of techniques for determining properties of programs without actually running them. Among the applications of static program analysis are the optimization by compilers of object code and the detection of malicious code or code that might be maliciously exploited. The obvious relevance and (sometimes critical) importance of such applications explain the many attempts to try to understand the general theoretical framework of static program analysis. Kleene algebra is the algebraic theory of finite automata and regular expressions. This algebraic tool has proven to be very suitable for the purpose of static analysis and verification of programs. The goal of this thesis is to develop an algebraic framework based on Kleene algebra to compute the solutions to a general class of intraprocedural dataflow analysis problems. The framework allows one to represent both the programs and the relevant properties in an homogeneous, compact and readable way. Traditional algorithms used to compute the result of an analysis are then replaced by algebraic manipulations of elements of a Kleene algebra