Structurer un interpréteur abstrait au moyen d'abstractions de valeurs et d'états :Eva, une analyse de valeur évoluée pour Frama-C

The formal verification of programs is nowadays a crucial challenge for computer science, as software bugs in critical systems may lead to catastrophic outcomes. Abstract interpretation is a general theory of approximation of the semantics of programming languages, practically used to detect errors in programs. Automatic analyses can be derived by computing an over-approximation of the possible behaviors of a program, through abstractions of its concrete semantics.This thesis proposes a new framework for the combination of multiple abstractions in the abstract interpretation theory. Its core concept is the structuring of the abstract semantics by following the usual distinction between expressions and statements. This can be achieved by a convenient architecture where abstractions are separated in two layers: value abstractions, in charge of the expression semantics, and state abstractions (or abstract domains), in charge of the statement semantics.This design leads naturally to an elegant communication system where the abstract states, when interpreting a statement, interact and exchange information through abstract values, that express properties about expressions. While the values form the communication interface between states, they are also standard elements of the abstract interpretation framework. The communication system is thus embedded in the abstract semantics, and the usual tools of abstract interpretation apply naturally to value abstractions. For instance, different kinds of value abstractions can be composed through the existing methods of combination of abstractions, enabling even further interaction between the components of the abstract semantics.This thesis explores the possibilities offered by this framework. We discuss efficient strategies to compute precise value abstractions from the properties inferred by abstract domains, and illustrate the means of communication between different state abstractions. Our architecture also features a direct collaboration for the emission of alarms that report the possible errors of a program.The general system of abstractions combination has been implemented within EVA, the new version of the abstract interpreter provided by the Frama-C platform. Thus, EVA enjoys a modular and extensible architecture designed to facilitate the introduction of new abstractions and to enable rich interactions between them. Thanks to this work, five new domains from the literature have been implemented in less than a year, enhancing both the scope and the precision of the analyzer.La vérification formelle de programmes est devenue un enjeu majeur de l'informatique, à l'heure où des erreurs logicielles dans des systèmes critiques peuvent avoir des conséquences dramatiques. L'interprétation abstraite est une théorie générale d'approximation des sémantiques des langages de programmation, qui permet des analyses automatiques de programmes pour en détecter de façon certaine les comportements indésirables. Ces analyses reposent sur des abstractions d'une sémantique concrète, qui calculent une sur-approximation des comportements possibles d'un programme.Cette thèse propose une nouvelle technique de composition modulaire entre les abstractions d'un interpréteur abstrait. L'idée principale en est l'organisation d'une sémantique abstraite suivant la distinction usuelle entre expressions et instructions. Les abstractions sont alors séparées entre abstractions de valeurs, en charge de la sémantique des expressions, et les abstractions d'états (ou domaines abstraits), en charge de la sémantique des instructions.Cette adéquate hiérarchie guide les interactions entre abstractions durant l'analyse. Lors de l'interprétation d'une instruction, les états abstraits peuvent échanger des informations au moyen de valeurs abstraites, qui expriment des propriétés sur les expressions. Ces valeurs abstraites forment donc l'interface de communication entre les domaines, mais sont également des éléments canoniques de l'interprétation abstraite. Les outils standards de la théorie s'appliquent donc naturellement aux abstractions de valeurs. En particulier, elles peuvent elle-mêmes être composées par les techniques existantes, ouvrant la voie à plus d'interactions encore.Cette thèse explore les possibilités offertes par cette nouvelle architecture des sémantiques abstraites. Elle décrit en particulier des stratégies efficaces pour le calcul de valeurs abstraites précises à partir des propriétés inférées par les domaines, et illustre les différents moyens d’interactions que ce système offre. Notre architecture comprend également une collaboration directe des différentes abstractions à l'émission des alarmes qui signalent les erreurs possibles d'un programme. Ce système de composition des abstractions a été mis en œuvre dans EVA, la nouvelle version de l'interpréteur abstrait de la plateforme Frama-C. EVA a été spécifiquement conçu pour faciliter l’introduction de nouvelles abstractions, et permettre des interactions riches entre ces abstractions. Grâce à son architecture modulaire et extensible, cinq nouveaux domaines abstraits ont pu être introduits dans l’analyseur en moins d’un an, améliorant ainsi tant ses capacités que sa précision