L’analyse statique de programmes est un domaine crucial en compilation, en optimisation, et en validation de logiciels. Les structures de données complexes (tableaux, listes, graphes...), omniprésentes dans les programmes, posent des problèmes difficiles, du fait qu’elles représentent des ensembles de données de taille importante ou inconnue, et que l’adressage des données dans ces ensembles est calculé (indexation, indirection). La plupart des travaux sur l’analyse des structures de données concernent la vérification de la correction des accès aux données (vérification que les indices d’un tableau sont dans les bornes, que les pointeurs ne sont pas nuls, “shape analysis”). L’analyse du contenu des structures de données est encore peu abordée. A Verimag, ce domaine a été abordé récemment, et a donné lieu à de premiers résultats sur l’analyse de tableaux unidimensionnels. Une méthode d’analyse de programmes simples a été proposée [1], qui permet de découvrir des propriétés des contenus de tableaux, comme par exemple que le résultat d’un programme de tri est bien un tableau trié. Un autre type de propriétés, dites “non positionnelles” a aussi été considéré [2], qui concerne le contenu global d’un tableau, indépendamment de son rangement: par exemple, on montre que le résultat d’un tri est une permutation du tableau initial. Ces premiers résultats sont très encourageants, mais encore embryonnaires. L’objectif du travail de thèse proposé est de les étendre dans plusieurs directions. Notre analyse de propriétés positionnelles est capable de découvrir des relations point- à-point entre des “tranches” de tableaux (ensembles de cellules consécutives). Les extensions envisagées concernent les tableaux multidimensionnels, les ensembles de cellules non nécessairement consécutives, et les structures de données plus générales. Concernant les propriétés non positionnelles, les premiers résultats sont limités aux égalités de contenus de tableaux. Ils doivent être étendus à des relations plus complexes (inclusions, sommes disjointes...) et à d’autres structures de données. Ce travail prend place dans le projet ASOPT (“Analyse statique et optimisation”), accepté dans le programme Arpège de l’ANR en 2008. Références : [1] N. Halbwachs, M. Péron. Discovering properties about arrays in simple programs. ACM Conference on Programming Language Design and Implementation, PLDI 2008. Tucson (Az.), juin 2008. [2] V. Perrelle. Analyse statique du contenu de tableaux, propriétés non positionnelles. Rapport de M2R, Master Parisien de Recherche en Informatique, septembre 2008. / Static analysis is key area in compilation, optimization and software validation. The complex data structures (arrays, dynamic lists, graphs...) are ubiquitous in programs, and can be challenging, because they can be large or of unbounded size and accesses are computed. (through indexing or indirections). Whereas the verification of the validity of the array accesses was one of the initial motivations of abstract interpretation, the discovery of properties about array contents was only adressed recently. Most of the analyses of array contents are based on a partitioning of the arrays. Then, they try to discover properties about each fragment of this partition. The choice of this partition is a difficult problem and each method have its flaw. Moreover, classical representations of array partitions induce an exponential complexity for these analyzes. In this thesis, we generalize the concept of array partitioning into the concept of "fragmentation" which allow overlapping fragments, handling potentially empty fragments and selecting specialized relations. On the other hand, we propose an abstraction of these fragmentations in terms of graphs called "slices diagrams" as well as the operations to manipulate them and ensuring a polynomial complexity. Finally, we propose a new criterion to compute a semantic fragmentation inspired by the existing ones which attempt to correct their flaws. These methods have been implemented in a static analyzer. Experimentations shows that the analyzer can efficiently and precisly prove some challenging exemples in the field of static analysis of programs manipulating arrays.

Ce travail a pour objectif d'éclaircir, par la voie d'une enquête sur le langage de l'action intentionnelle et la grammaire des concepts psychologiques, la nature de notre capacité ordinaire à assigner un sens aux actions humaines et les conditions de son exercice. À l'heure actuelle, les débats sont dominés par une conception causaliste de l'action et de son explication qui innerve des problèmes tels que celui de la causalité mentale, de la réalité des états mentaux ou du statut de la « psychologie populaire ». Le causalisme pose que la différence entre une action et un simple mouvement corporel tient au fait que la première est causée par certains antécédents mentaux, distincts du mouvement, qui rendent compte de son caractère intentionnel. Expliquer une action consisterait dès lors à donner des raisons référant à ces états. Renouant avec l'approche logico-grammaticale issue de Wittgenstein et développée par Anscombe, nous entendons montrer que cette conception est erronée. Son principal défaut est de succomber à une image mentaliste selon laquelle les prédicats psychologiques utilisés dans les explications ordinaires ont toujours pour fonction de dénoter des états, des processus ou des événements internes à l'agent, distincts de l'action et pouvant entrer dans des chaînes causales. Contre cela, nous voulons établir que la différence entre action et mouvement corporel est une différence entre deux modes de description. Le mode intentionnel dans lequel se disent les actions se caractérise de façon essentielle par l'asymétrie de la première et de la troisième personnes. Expliquer une action consiste à en donner une description qui l'identifie dans sa dimension téléologique. Notre démarche est la suivante. Le premier mouvement de notre étude est consacré à la clarification des liens conceptuels entre intention et action. Après avoir rappelé les origines modernes de la conception causaliste, nous critiquons les arguments proposés par Davidson en sa faveur. Récusant leur mentalisme sous-jacent, nous montrons que le caractère intentionnel d'une action ne dépend pas de la présence d'un « ingrédient » mental. Puis nous rendons compte de la force explicative des descriptions intentionnelles en les mettant en rapport avec la spécificité du raisonnement pratique et de la connaissance d'agent. Dans un second mouvement, nous revenons sur la nature de la capacité à formuler des jugements psychologiques au sujet d'autrui. Nous examinons successivement la thèse selon laquelle les agents possèdent une théorie de l'esprit et celle selon laquelle ils recourent à un principe de charité interprétative. Contre ces approches intellectualistes, nous soutenons que l'usage sensé des termes psychologiques est un savoir-faire qui doit être mis en relation avec l'expressivité naturelle du corps humain, la dimension intrinsèquement sociale et institutionnelle de la vie humaine et l'existence de formes d'action et d'expression partagées faisant autorité. Reconnaître les conditions actionnelles de l'intelligibilité d'autrui exige de se défaire de l'illusion moderne d'un « sujet désengagé ». / My objective is to elucidate, by means of a grammatical inquiry into the language of intentional action and the use of psychological concepts, the nature of our ordinary capacity to make sense of human actions, as well as the conditions of its exercise. In contemporary debates prevails a causalist view of action and its explanation, which underlies the discussions about mental causation, the reality of mental states or the epistemic status of so-called folk psychology. Causalism holds that an action differs from a mere bodily movement by its being caused by some mental antecedents, distinct from movement, which account for its intentional character. Explaining an action would thus consist in giving reasons ultimately referring to those states. In line with the wittgensteinian logico-grammatical approach developed by Anscombe, I intend to show that this view is misconceived. Its main defect lies in its mentalism, i.e. the tendency to see psychological predicates as always functioning to denote internal episodes or events, distinct from action and liable to figure in causal chains as links bringing about the agent's behaviour. Against this, I want to establish that the distinction between action and mere movement is to be seen as a difference between two modes of description. The intentional mode in which are couched action descriptions is essentially characterized by the first/third-person asymmetry. Explaining an action consists in identifying it by a description exhibiting its teleological features. My plan is the following. The first main move is to clarify the conceptual relations between intention and action. Having brought to light the modern roots of causalism, I consider the arguments Davidson put forward in its favour, so as to refute their underlying mentalism. I show that for an action, being intentional does not depend on any occurrence of a separate mental component. Then I proceed to account for the explanatory force of intentional descriptions by relating them to the specificity of practical reasoning and agent knowledge. The second main move tackles the question to know what the capacity of making sense of others consists in. I successively consider the idea that agents possess a theory of mind and the thesis as to which they must rely on a principle of interpretative charity. Against those intellectualist views, I claim that sensible use of psychological concepts is a practical skill which is to be related to the sensibility to the natural expressivity of human body, the intrinsically social and institutional features of human life and the existence of shared standards of expression and action. Acknowledging the action-based conditions of others' intelligibility requires to dispose of the modern illusion of a « disengaged subject ».

La rapidité, la consommation énergétique et l'efficacité des systèmes logiciels et matériels sont devenues les préoccupations majeures de la communauté informatique de nos jours. Gérer de manière correcte et efficace les problématiques mémoire est essentiel pour le développement des programmes de grande tailles sur des architectures de plus en plus complexes. Dans ce contexte, cette thèse contribue aux domaines de l'analyse mémoire et de la compilation tant sur les aspects théoriques que sur les aspects pratiques et expérimentaux. Outre l'étude approfondie de l'état de l'art des analyses mémoire et des différentes limitations qu'elles montrent, notre contribution réside dans la conception et l'évaluation de nouvelles analyses qui remédient au manque de précision des techniques publiées et implémentées. Nous nous sommes principalement attachés à améliorer l'analyse de pointeurs appartenant à une même structure de données, afin de lever une des limitations majeures des compilateurs actuels. Nous développons nos analyses dans le cadre général de l'interprétation abstraite « non dense ». Ce choix est motivé par les aspects de correction et d'efficacité : deux critères requis pour une intégration facile dans un compilateur. La première analyse que nous concevons est basée sur l'analyse d'intervalles des variables entières ; elle utilise le fait que deux pointeurs définis à l'aide d'un même pointeur de base n'aliasent pas si les valeurs possibles des décalages sont disjointes. La seconde analyse que nous développons est inspirée du domaine abstrait des Pentagones ; elle génère des relations d'ordre strict entre des paires de pointeurs comparables. Enfin, nous combinons et enrichissons les deux analyses précédentes dans un cadre plus général. Ces analyses ont été implémentées dans le compilateur LLVM. Nous expérimentons et évaluons leurs performances, et les comparons aux implémentations disponibles selon deux métriques : le nombre de paires de pointeurs pour lesquelles nous inférons le non-aliasing et les optimisations rendues possibles par nos analyses / This thesis was motivated by the emergence of massively parallel processing and supercomputingthat tend to make computer programming extremely performing. Speedup, the power consump-tion, and the efficiency of both software and hardware are nowadays the main concerns of theinformation systems community. Handling memory in a correct and efficient way is a step towardless complex and more performing programs and architectures. This thesis falls into this contextand contributes to memory analysis and compilation fields in both theoretical and experimentalaspects.Besides the deep study of the current state-of-the-art of memory analyses and their limitations,our theoretical results stand in designing new algorithms to recover part of the imprecisionthat published techniques still show. Among the present limitations, we focus our research onthe pointer arithmetic to disambiguate pointers within the same data structure. We develop ouranalyses in the abstract interpretation framework. The key idea behind this choice is correctness,and scalability: two requisite criteria for analyses to be embedded to the compiler construction.The first alias analysis we design is based on the range lattice of integer variables. Given a pair ofpointers defined from a common base pointer, they are disjoint if their offsets cannot have valuesthat intersect at runtime. The second pointer analysis we develop is inspired from the Pentagonabstract domain. We conclude that two pointers do not alias whenever we are able to build astrict relation between them, valid at program points where the two variables are simultaneouslyalive. In a third algorithm we design, we combine both the first and second analysis, and enhancethem with a coarse grained but efficient analysis to deal with non related pointers.We implement these analyses on top of the LLVM compiler. We experiment and evaluate theirperformance based on two metrics: the number of disambiguated pairs of pointers compared tocommon analyses of the compiler, and the optimizations further enabled thanks to the extraprecision they introduce

Le répertoire original pour harpe est relativement restreint. Deux voies permettent de concourir à son accroissement : la création contemporaine d’une part, et la transcription d’autre part. La présente étude interroge le rapport entre les habitus anciens et une pratique actuelle de transcription, depuis le répertoire de clavecin français du XVIIIe siècle vers la harpe. La transcription est ici considérée comme une pratique non notée qui relève de l’interprétation, et qui partage avec celle-ci, comme avec la traduction, des problématiques fondamentales en apparence antinomiques : esprit et lettre, idiomatisme et fidélité. Elle confronte l’interprète à ses propres limites ainsi qu’à celles de son instrument, et favorise la rencontre avec l’altérité d’une écriture dépourvue de gestes familiers. La transcription constitue l’un des moyens privilégiés de compréhension du répertoire transcrit, de l’instrument de destination, et du rapport de l’interprète à son instrument. La transcription du répertoire de clavecin français pour harpe sera envisagée tout d’abord sous un angle historique, puis à travers les interrogations de nature esthétique que suscite l’antagonisme entre idiomatisme et fidélité, enfin la question des limites et impossibilités sera interrogée selon une approche technique et pratique. / The original harp repertoire is rather limited. It seems there are two efficient ways to help its increase : contemporary creation on the one hand, and transcription on the other. This study questions the relation between early music and a current way of transcribing for harp the eighteenth century french harpischord repertoire. Transcription is here considered as an unwritten practice that comes close to interpretation, and like interpretation and translation, it faces fundamental issues which seem paradoxical : spirit and letter, idiomatism and fidelity. Transcription forces the performer to face his own limits as well as his intrument’s, and it favours the encounter with the otherness of a writing that is free of any familiar gesture. Transcription is one of the best ways to comprehend the transcribed repertoire, the instrument the piece is being transcribed for, and the relationship the performer has with his instrument. The transcription for harp of the eighteenth century french harpischord repertoire will be examined first under a historic angle, then, with esthetic concerns raised by the paradox between idiomatism and fidelity, and finally, the issue of the limits and impossibilities will be studied from a technical and practical approach.

Examinando-se a idéia romana da auctoritas, encontra-se nela o registro, em linguagem mítica, da experiência de superação do conflito de vontades antagônicas e da instalação de um espaço horizontal em que se torna possível, graças ao julgamento e à ação, fundar as bases de um novo agir conjunto. Tal perspectiva permite analisar em chave distinta as relações entre direito e poder, abrindo espaço para a compreensão do direito como um fenômeno plural e dotado de dramaticidade, em cujo centro a figura do legislador racional, forjada a partir da experiência jurídica, não comunica potestas aos interlocutores jurídicos, mas sim a auctoritas de uma linguagem em que as mensagens de uns a outros podem ser traduzidas, nenhuma delas pode ser ignorada, e mesmo aquelas que não se traduzem em decisões prosseguem dotadas de força comunicativa. Investiga-se em seguida o direito como palco de representação, confronto, reformulação e ajuste de interesses, identificando-se o processo como órgão de que a civitas se vale para captar o político, e o populus representado para expressar o seu julgamento a respeito dos resultados globais da representação jurídica e política - eventualmente ensejador da mobilização de regras de calibração para a emissão, pelos comunicadores normativos, de respostas dotadas de auctoritas, e afinadas com os problemas apresentados pelas partes. Passa-se então ao exame da relação entre o vigor das normas jurídicas e a liberdade dos cives, mostrando-se que o êxito pragmático da comunicação normativa não se relaciona à imposição potestativa de um sentido único, mas à manutenção de um espaço em que se oferece aos cives, como alternativa aos riscos de violência e dominação do campo político, a possibilidade - e a liberdade - da ação dentro do sistema jurídico. / En examinant l\'idée romaine d\'auctoritas, on y trouve le rapport, en langage mythique, de l\'expérience du dépassement du conflict des volontés antagoniques et de l\'tablissement d\'un espace horizontal oùl il devient possible, grâce au jugement et à l\'action, fonder les bases d\'un nouveau agir conjoint. Cela rend possible une analyse distincte des rélations entre le droit et le pouvoir, et la compréension du premier comme un phénomène pluriel et doué de la dynamique d\'un drame, au coeur duquel la figure du legislateur rationnel, báti au sein de l\'experience juridique, ne communique point de potestas aux interlocuteurs juridiques, mais si l\'auctoritas d\'un langage où les uns peuvent traduire ce que les autres leur disent, où aucune message ne peut pas être ignorée et où même celles qui ne réussissent pas à fonder des décisions conservent leur force communicative. On examine ensuite le droit comme scène de representation, confrontation, reformulation et ajustement d\'interêts, et l\'on reussit à identifier le procéss comme organe dont la civitas se serl pour saisir le champ politique, et dont le populus representé se vaut pour exprimer son jugement sur les resultés de l\'activité des representants des champs juridique et politique. Ce jugement peut, à la limite, mettre en mouvement des règles de calibrage, qui assurent l\'auctoritas des reponses des communicateurs normatifs et leur consonance avec les problèmes soulevés par les parts du procés. L\'on reflet ensuite sur la relation entre la vigueur des règles de droit et la liberté des cives, et l\'on voit que le succès pragmatique de la communication normative n\'equivaut pas à l\'imposition potestative d\'un sens unique, mais plutôt à la manutention d\'un espace où les cives jouissent de la possibilité et de la liberté de l\'action dans le systhème juridique, comme voie alternative aux risques de violence et de domination du champ politique.

Résumé en français Le personnage homosexuel masculin dans le théâtre en France au cours du XXème siècle a singulièrement évolué. Nous analyserons d’une part, les typologies de ce personnage, à travers huit pièces. D’autre part, pour chacune d’entre elles, nous verrons comment la presse et les publics ont interprété ces personnages. Nous verrons comment, au delà de la forme théâtrale, c’est tout un discours sur les homosexuels qui est donné à voir et qui vient par là interroger les rapports entre le théâtre et la société. Dans la première partie de notre présente étude nous avons présenté le personnage homosexuel dans trois pièces, de facture différente, mais qui donnent toutes les trois à voir une figure de solitaire : Le Monsieur aux Chrysanthèmes, Armory, Un Taciturne de Roger Martin du Gard er Adam de Marcel Achard.. Il est solitaire car emmuré dans une tradition qui le condamne pour son désir alors même qu’il est resté inassouvi. L’homosexualité serait donc la marque d’un esprit faible, qui ne sait pas taire ses penchants et ne s’y employant pas suffisamment bien, se suicide.La deuxième partie de notre travail s’est penchée sur le personnage homosexuel présenté comme source de comique. Il s’agira le plus souvent de montrer que le rire qu’il suscite est une autre forme de condamnation par la société. Il s’agit alors d’un mode mineur, moins violent apparemment, mais tout aussi significatif d’un regard porté par la société sur les homosexuels. Cette partie est centrée sur les pièces d’Edouard Bourdet, La Fleur des Pois, d’André Roussin, Les Œufs de l’Autruche et enfin de Jean Poiret, La Cage aux folles. Le personnage homosexuel fait rire car il est incapable de se conformer à ce que la société, implicitement, attend de lui. Un homme doit, naturellement aimer les femmes, être viril, masculin, maîtriser ses sentiments et ses émotions, ne pas pleurer. Dans notre dernière partie, apparaîtra, pour la première fois, une réappropriation qui va se faire par les homosexuels eux mêmes et, de ce fait, ouvrir la voie à d’autres artistes qui ne parleront pas à la place des homosexuels. Au contraire, naîtront des formes qui seront revendiquées comme étant écrites par des homosexuels. C’est le cas avec les deux dernières pièces que nous avons réunies dans notre corpus : Angels in America de Tony Kushner et Le Pays Lointain de Jean-Luc Lagarce. Elles évoquent, de manière plus directe pour la première, l’épidémie de SIDA dans les années 1980 et 1990 au sein de la communauté homosexuelle. / In the XXth century, in French theatre, the gay male character has remarkably changed. We will analyse on one hand the character typologies across eight plays. One the other hand, for each of the plays we will see how the public and the press interpreted these characters. We will see, above the theatrical form, how it finally is a speech on homosexual that is given and that comes and asks the links that are between theatre and society.In the first part of our study we introduced, the gay male character in three plays, with different styles but the three of them will give a solitary figure : Le Monsieur aux Chrysanthèmes of Armory, Un taciturne of Roger Martin and Adam of Marcel Achard. It is a solitary character because it is walled in a tradition that condemns it for its own desire where it is already unfulfilled. Homosexuality will then be seen as the mark of a weak spirit, that can not shut its inclinations and when it’s too obvious the character will commit suicide.The second part of our work underlines gay male character seen as a comic part. The point will show how the character generates laughter, and so, it does prove society condemnation. It is a minor mode indeed, apparently less violent, but it just shows how society sees homosexuals, in an other way . This part will be focused on 3 plays : La Fleur des Pois of Edouard Bourdet,, Les Oeufs de l’Autruche of André Roussi and La Cage aux folles of Jean Poiret. The homosexual character does make laugh because it is unable to conform to what society really expects from him. A man has to love a woman, be manly, masculine, he has to master his feelings and not cry.In our last part will appear for the first time, an acquisition of homosexual signs. Thanks to that other artists will not talk instead of homosexuals. On the contrary, some forms will be born and they will be claimed as written by homosexuals. It is the case in the last two plays we gathered in our corpus: Angels in America of Tony Kushner and Le Pays Lointain of Jean-Luc Lagarce. They both talk, in a more direct way, of the AIDS epidemic in the 80’s and 90’s among the homosexual community.

Doctorat en philosophie et lettres / info:eu-repo/semantics/nonPublished

Doctorat en philosophie et lettres / info:eu-repo/semantics/nonPublished

Qu'est-ce qui fait de la philosophie une discipline autonome par rapport aux sciences ? Centrale dans l’œuvre de Granger, cette question nous conduira à examiner l'opposition entre deux procédés : la structuration scientifique et l'interprétation philosophique. La première construit l'expérience dans des structures d'objets, tandis que la seconde la commente dans des systèmes de significations. Nous montrerons comment ces deux procédés prolongent une distinction plus fondamentale qui se situe au niveau même de la réalité : le virtuel et l'actuel. En reconnaissant que le parcours de la connaissance est un va-et-vient constant entre l'actualité brute de l'expérience et sa virtualité construite, le chemin de la science à la philosophie se tracera ainsi : au point de départ - les sciences formelles - lieu de naissance du virtuel ; à une étape intermédiaire - les sciences empiriques - moment de confrontation du virtuel à l'actuel ; à l'aboutissement - la philosophie - champ d'unification de la réalité dans la totalité de ses aspects. / What makes philosophy an autonomous discipline regarding sciences? Central in the oeuvre of Granger, this question will lead us to examine the opposition between two procedures: the scientific structuration and the philosophical interpretation. The first builds the experience in structures of objects, whereas the second comments it in systems of significations.We will demonstrate how these two procedures extend a more fundamental distinction that lies in the very level of reality: the virtual and the actual. Acknowledging that the course of knowledge is a constant back and forth between the crude actuality of experience and its built virtuality, the way from science to philosophy can be drawn as follows: at the starting point - formal sciences - birthplace of virtual; to an intermediate stage - the empirical sciences - moment of confrontation between the virtual and the actual; and ultimately - the philosophy - unification field of the reality in the totality of its aspects.

Cette thèse propose un nouveau cadre pour la composition de domaines abstraits. L'idée principale en est l'organisation d'une sémantique abstraite suivant la distinction usuelle entre expressions et instructions, en cours dans la plupart des langages impératifs. La définition d'une sémantique abstraite peut alors se diviser entre abstractions de valeurs et abstractions d'états (ou domaine abstrait). Les abstractions de valeurs représentent les valeurs possibles d'une expression en un point donné, et assurent l'interprétation de la sémantique des expressions. Les abstractions d'états représentent les états machines qui peuvent se produire lors de l'exécution d'un programme, et permettent d'interpréter la sémantique des instructions. De ce choix de conception découle naturellement un élégant système de communication entre abstractions. Lors de l'interprétation d'une instruction, les abstractions d'états peuvent échanger des informations au moyen d'abstractions de valeurs, qui expriment des propriétés à propos des expressions. Les valeurs forment donc une interface de communication entre états abstraits, mais sont également des éléments canoniques de l'interprétation abstraite. Ils peuvent donc eux-même être combinés par les moyens existants de composition d'abstractions, permettant encore davantage d'interactions entre les composants des sémantiques abstraites. Cette thèse explore les possibilités offertes par cette nouvelle architecture des sémantiques abstraites. Nous décrivons en particulier des stratégies efficaces pour le calcul d'abstractions de valeurs précises à partir des propriétés inférées par les domaines, et nous illustrons les différentes possibilités d'interactions que ce système offre. L'architecture que nous proposons inclue également une collaboration directe des abstractions pour l'émission des alarmes qui signalent les erreurs possibles du programme analysé. Nous proposons également un mécanisme permettant d'interagir avec les composants d'une combinaison générique de types OCaml. Nous utilisons des GADT pour encoder la structure interne d'une combinaison, et construisons automatiquement les fonctions d'injection et de projection entre le produit et ses composants. Cette fonctionnalité permet d'établir une communication directe entre les différentes abstractions d'un interpréteur abstrait. Enfin, une dernière contribution de cette thèse est l'extension automatique de domaines abstraits à l'aide de prédicats logiques qui évitent les pertes d'information aux points de jonction. De fait, lorsque plusieurs chemins d'exécution se rejoignent, un domaine abstrait doit représenter les comportements possibles de chacun des chemins, ce qui engendre souvent des pertes de précision. Pour remédier à cette limitation, nous proposons de propager un ensemble d'états abstraits, munis chacun d'un prédicat qui indique sous quelle condition l'état est valable. Contrairement à d'autres approches, notre analyse ne maintient pas une stricte partition des états abstraits, car les prédicats utilisés ne sont pas mutuellement exclusifs. Cette particularité rend possible des optimisations cruciales pour le passage à l'échelle de cette technique, confirmée par nos résultats expérimentaux sur un programme industriel généré. L'ensemble du système de composition des abstractions proposé dans cette thèse a été mis en œuvre dans EVA, la nouvelle version de l'interpréteur abstrait de 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 introduit dans l'analyseur en moins d'un an, améliorant ainsi tant ses capacités que sa précision. / This thesis proposes a new framework for the combination of multiple domains 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 domains, when interpreting a statement, interact and exchange information through value abstractions, that express properties about expressions. While the values form the communication interface between domains, 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 information 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. We also proposes a mechanism to enable interacting with the components of a modular combination of OCaml types. We use GADT to encode the inner shape of a combination, and automatically build injection and projection functions between a product of datatypes and its components. This allows direct communications between the abstractions of an abstract interpreter. Finally, a last contribution of this thesis is the automatic extension of abstract domains to track sets of disjunctive abstract states, each one being qualified with a predicate for which the state holds. This enhances the precision of an abstract semantics at join points, when several possible paths of a program execution meet. At these points, predicates preserve the information usually lost by the merge of abstract states. Unlike other approaches, the analysis does not maintain a strict partition of the abstract states, as the predicates we use are not mutually exclusive. This design enables some optimizations that are crucial for scalability, as confirmed by our experimental results on an industrial, generated 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 the scope and the precision of the analyzer.