En C, une stratégie classique pour implémenter les codes de gestion d'erreur est de faire suivre chaque opération qui peut générer une erreur d'une structure conditionnelle qui teste si l'opération a renvoyé une erreur. Ce stratégie basique, cependant, est sujette à erreurs, et il est courant d'oublier des opérations de nettoyage requises, ainsi que d'oublier de mettre à jour des codes de gestion d'erreur existants lorsque la fonction est étendue avec de nouvelles opérations. De plus, une partie importante du code doit souvent être dupliquée. Un style de programmation, <EM> stratégie goto </EM>, qui peut réduire en partie certaines de ces difficultés. Pour améliorer la structure des codes de gestion d'erreur dans les logiciels système, nous définissions un algorithme qui permet de transformer les codes de gestion d'erreur implémentés suivant la stratégie basique en codes de gestion d'erreur qui utilisent la <EM> stratégie goto</EM>. Même lorsque les codes de gestion d'erreurs sont structurés, la gestion et la libération des ressources allouées restent un problème lorsqu'il s'agit d'assurer la robustesse du code système. Dans cette thèse, nous proposons un algorithme <EM> microscopique </EM> de détection d'omission de libération de ressource, basé sur une analyse principalement intra-procédurale, qui prend en compte les flux et les chemins du code et qui cible et exploite les propriétés des codes de gestion d'erreur. Notre algorithme est résistant aux faux positifs dans l'ensemble des acquisitions de ressources et des opérations de libération, ce qui produit un faible taux de faux positifs dans les rapports renvoyés par l'outil tout en passant à l'échelle.

L’amélioration des performances des robots est un enjeu important dans le domaine industriel. Les objectifs visés sont l’augmentation de l’espace de travail, de la capacité de charge transportable, de la vitesse de travail et de la précision du robot. Pour atteindre ces objectifs, il faut en général augmenter la rigidité, diminuer la masse et augmenter la capacité d’amortissement du robot. Les robots actuels sont généralement fabriqués en métaux : aluminium ou acier, ce qui limite leurs performances en raison des faibles capacités d’amortissement des vibrations de ces matériaux. Les matériaux composites présentent l’avantage de combiner des matériaux différents, ce qui conduit à une variété de leurs performances. Parmi les types de renforts, les fibres de carbone présentent un module d’élasticité élevé permettant la conception de pièces de grandes rigidités statiques mais elles possèdent une faible capacité d’amortissement. Les fibres végétales, par contre, possèdent une faible densité, de bonnes propriétés spécifiques et des capacités d’amortissement élevées. Cette thèse porte sur l’amélioration des performances d’un robot parallèle 3CRS en utilisant des matériaux composites pour reconcevoir des pièces initialement fabriquées en aluminium. La thèse commence d’abord par une caractérisation des comportements statiques et dynamiques du robot initial constitué de bras en aluminium. Ensuite, la forme des segments des bras robotiques est optimisée par rapport aux sollicitations mécaniques sur le robot. Un nouveau composite stratifié hybride renforcé par des fibres de carbone et des fibres de lin est alors proposé. Cette combinaison permet d’allier les avantages des deux types de fibres dans un composite pour le dimensionnement des composants sous sollicitation élevée. La structure de ce nouveau composite a été optimisée puis un segment est fabriqué pour valider la conception. Finalement, l’étude du nouveau robot avec des bras en matériaux composites a été réalisée, les résultats montrent que la rigidité du robot augmente, sa masse diminue légèrement et sa capacité d’amortissement augmente considérablement par rapport au robot initial. Donc, l’application du composite stratifié hybride peut améliorer les performances statiques et dynamiques et augmenter significativement la précision en fonctionnement du robot 3CRS. / Improvement of the robot’s performances is a major challenge in the industrial field. In general, improvement objectives are increasing workspace, transportable capacity, speed and precision of the robot. To achieve these objectives, it must increase rigidity, reduce weight and increase damping capacity of the robot. Currently, the robots are generally made of metals: aluminum or steel, which limits their performances due to low damping capacity of these materials.Composite materials present an advantage to combine different materials, which leads to a variety of composite material properties. Among the types of reinforcements, carbon fibers show high modulus that enables robotic parts with high static rigidities to be designed. However, carbon fibers have generally a low damping capacity. Natural fibers have low density, good specific properties and high damping capacity.This thesis focuses on the improvement of the performances of the 3CRS parallel robot by using the composite material to redesign robot parts initially made of aluminum. The thesis begins with static and dynamic characterizations of the original robot. Then, the shape of segments of the robotic arms is optimized with respect to applying force on the robot. A hybrid laminated composite reinforced with carbon fibers and flax fibers is proposed for the use. This combination enables to combine the advantages of two fiber types in a composite for using in high loaded components. The structure of the new hybrid laminated composite is optimized and a composite segment is then fabricated in order to validate the design. Finally, the analysis of the new robot with composite arms is executed. The result shows that the new robot has a slightly higher rigidity, lighter mass and considerably greater damping capacity in comparison with the original robot. Therefore, the application of the hybrid composite could improve the static and dynamic performances and increases considerably the accuracy in operation of the robot 3CRS.

L'analyse statique de programme a pour but de prouver automatiquement qu'un programme vérifie certaines propriétés. L'interprétation abstraite est un cadre théorique permettant de calculer des invariants de programme. Ces invariants sont des propriétés sur les variables du programme vraies pour toute exécution. La précision des invariants calculés dépend de nombreux paramètres, en particulier du domaine abstrait et de l'ordre d'itération utilisés pendant le calcul d'invariants. Dans cette thèse, nous proposons plusieurs extensions de cette méthode qui améliorent la précision de l'analyse.Habituellement, l'interprétation abstraite consiste en un calcul de point fixe d'un opérateur obtenu après convergence d'une séquence ascendante, utilisant un opérateur appelé élargissement. Le point fixe obtenu est alors un invariant. Il est ensuite possible d'améliorer cet invariant via une séquence descendante sans élargissement. Nous proposons une méthode pour améliorer un point fixe après la séquence descendante, en recommençant une nouvelle séquence depuis une valeur initiale choisie judiscieusement. L'interprétation abstraite peut égalementêtre rendue plus précise en distinguant tous les chemins d'exécution du programme, au prix d'une explosion exponentielle de la complexité. Le problème de satisfiabilité modulo théorie (SMT), dont les techniques de résolution ont été grandement améliorée cette décennie, permettent de représenter ces ensembles de chemins implicitement. Nous proposons d'utiliser cette représentation implicite à base de SMT et de les appliquer à des ordres d'itération de l'état de l'art pour obtenir des analyses plus précises.Nous proposons ensuite de coupler SMT et interprétation abstraite au sein de nouveaux algorithmes appelés Modular Path Focusing et Property-Guided Path Focusing, qui calculent des résumés de boucles et de fonctions de façon modulaire, guidés par des traces d'erreur. Notre technique a différents usages: elle permet de montrer qu'un état d'erreur est inatteignable, mais également d'inférer des préconditions aux boucles et aux fonctions.Nous appliquons nos méthodes d'analyse statique à l'estimation du temps d'exécution pire cas (WCET). Dans un premier temps, nous présentons la façon d'exprimer ce problème via optimisation modulo théorie, et pourquoi un encodage naturel du problème en SMT génère des formules trop difficiles pour l'ensemble des solveurs actuels. Nous proposons un moyen simple et efficace de réduire considérablement le temps de calcul des solveurs SMT en ajoutant aux formules certaines propriétés impliquées obtenues par analyse statique. Enfin, nous présentons l'implémentation de Pagai, un nouvel analyseur statique pour LLVM, qui calcule des invariants numériques grâce aux différentes méthodes décrites dans cette thèse. Nous avons comparé les différentes techniques implémentées sur des programmes open-source et des benchmarks utilisés par la communauté. / Static program analysis aims at automatically determining whether a program satisfies some particular properties. For this purpose, abstract interpretation is a framework that enables the computation of invariants, i.e. properties on the variables that always hold for any program execution. The precision of these invariants depends on many parameters, in particular the abstract domain, and the iteration strategy for computing these invariants. In this thesis, we propose several improvements on the abstract interpretation framework that enhance the overall precision of the analysis.Usually, abstract interpretation consists in computing an ascending sequence with widening, which converges towards a fixpoint which is a program invariant; then computing a descending sequence of correct solutions without widening. We describe and experiment with a method to improve a fixpoint after its computation, by starting again a new ascending/descending sequence with a smarter starting value. Abstract interpretation can also be made more precise by distinguishing paths inside loops, at the expense of possibly exponential complexity. Satisfiability modulo theories (SMT), whose efficiency has been considerably improved in the last decade, allows sparse representations of paths and sets of paths. We propose to combine this SMT representation of paths with various state-of-the-art iteration strategies to further improve the overall precision of the analysis.We propose a second coupling between abstract interpretation and SMT in a program verification framework called Modular Path Focusing, that computes function and loop summaries by abstract interpretation in a modular fashion, guided by error paths obtained with SMT. Our framework can be used for various purposes: it can prove the unreachability of certain error program states, but can also synthesize function/loop preconditions for which these error states are unreachable.We then describe an application of static analysis and SMT to the estimation of program worst-case execution time (WCET). We first present how to express WCET as an optimization modulo theory problem, and show that natural encodings into SMT yield formulas intractable for all current production-grade solvers. We propose an efficient way to considerably reduce the computation time of the SMT-solvers by conjoining to the formulas well chosen summaries of program portions obtained by static analysis.We finally describe the design and the implementation of Pagai,a new static analyzer working over the LLVM compiler infrastructure,which computes numerical inductive invariants using the various techniques described in this thesis.Because of the non-monotonicity of the results of abstract interpretation with widening operators, it is difficult to conclude that some abstraction is more precise than another based on theoretical local precision results. We thus conducted extensive comparisons between our new techniques and previous ones, on a variety of open-source packages and benchmarks used in the community.

Dans le domaine de la vérification formelle de logiciels, il est impératif d'identifier les limites au sein desquelles les éléments ou fonctions opèrent. Ces limites constituent les propriétés de frame (frame properties en anglais). Elles sont habituellement spécifiées manuellement par le programmeur et leur validité doit être vérifiée: il est nécessaire de prouver que les opérations du programme n'outrepassent pas les limites ainsi déclarées. Dans le contexte de la vérification formelle interactive de systèmes complexes, comme les systèmes d'exploitation, un effort considérable est investi dans la spécification et la preuve des propriétés de frame. Cependant, la plupart des opérations ont un effet très localisé et ne menacent donc qu'un nombre limité d'invariants. Étant donné que la spécification et la preuve de propriétés de frame est une tache fastidieuse, il est judicieux d'automatiser l'identification des invariants qui ne sont pas affectés par une opération donnée. Nous présentons dans cette thèse une solution inférant automatiquement leur préservation. Notre solution a pour but de réduire le nombre de preuves à la charge du programmeur. Elle est basée sur l'analyse statique, et ne nécessite aucune annotation de frame. Notre stratégie consiste à combiner une analyse de dépendances avec une analyse de corrélations. Nous avons conçu et implémenté ces deux analyses statiques pour un langage fonctionnel fortement typé qui manipule structures, variants et tableaux. Typiquement, une propriété fonctionnelle ne dépend que de quelques fragments de l'état du programme. L'analyse de dépendances détermine quelles parties de cet état influent sur le résultat de la propriété fonctionnelle. De même, une fonction ne modifiera que certaines parties de ses arguments, copiant le reste à l'identique. L'analyse de corrélations détecte quelles parties de l'entrée d'une fonction se retrouvent copiées directement (i.e. non modifiés) dans son résultat. Ces deux analyses calculent une approximation conservatrice. Grâce aux résultats de ces deux analyses statiques, un prouveur de théorèmes interactif peut inférer automatiquement la préservation des invariants qui portent sur la partie non affectée par l’opération concernée. Nous avons appliqué ces deux analyses statiques à la spécification fonctionnelle d'un micro-noyau, et obtenu des résultats non seulement d'une précision adéquate, mais qui montrent par ailleurs que notre approche peut passer à l'échelle. / In the field of software verification, the frame problem refers to establishing the boundaries within which program elements operate. It has notoriously tedious consequences on the specification of frame properties, which indicate the parts of the program state that an operation is allowed to modify, as well as on their verification, i.e. proving that operations modify only what is specified by their frame properties. In the context of interactive formal verification of complex systems, such as operating systems, much effort is spent addressing these consequences and proving the preservation of the systems' invariants. However, most operations have a localized effect on the system and impact only a limited number of invariants at the same time. In this thesis we address the issue of identifying those invariants that are unaffected by an operation and we present a solution for automatically inferring their preservation. Our solution is meant to ease the proof burden for the programmer. It is based on static analysis and does not require any additional frame annotations. Our strategy consists in combining a dependency analysis and a correlation analysis. We have designed and implemented both static analyses for a strongly-typed, functional language that handles structures, variants and arrays. The dependency analysis computes a conservative approximation of the input fragments on which functional properties and operations depend. The correlation analysis computes a safe approximation of the parts of an input state to a function that are copied to the output state. It summarizes not only what is modified but also how it is modified and to what extent. By employing these two static analyses and by subsequently reasoning based on their combined results, an interactive theorem prover can automate the discharching of proof obligations for unmodified parts of the state. We have applied both of our static analyses to a functional specification of a micro-kernel and the obtained results demonstrate both their precision and their scalability.

Une des étapes les plus cruciales dans le processus d’analyse des performances d’une application est la détection des goulets d’étranglement. Un goulet étant tout évènement qui contribue à l’allongement temps d’exécution, la détection de ses causes est importante pour les développeurs d’applications afin de comprendre les défauts de conception et de génération de code. Cependant, la détection de goulets devient un art difficile. Dans le passé, des techniques qui reposaient sur le comptage du nombre d’évènements, arrivaient facilement à trouver les goulets. Maintenant, la complexité accrue des micro-architectures modernes et l’introduction de plusieurs niveaux de parallélisme ont rendu ces techniques beaucoup moins efficaces. Par conséquent, il y a un réel besoin de réflexion sur de nouvelles approches.Notre travail porte sur le développement d’outils d’évaluation de performance des boucles de calculs issues d’applications scientifiques. Nous travaillons sur Decan, un outil d’analyse de performance qui présente une approche intéressante et prometteuse appelée l’Analyse Décrémentale. Decan repose sur l’idée d’effectuer des changements contrôlés sur les boucles du programme et de comparer la version obtenue (appelée variante) avec la version originale, permettant ainsi de détecter la présence ou pas de goulets d’étranglement.Tout d’abord, nous avons enrichi Decan avec de nouvelles variantes, que nous avons conçues, testées et validées. Ces variantes sont, par la suite, intégrées dans une analyse de performance poussée appelée l’Analyse Différentielle. Nous avons intégré l’outil et l’analyse dans une méthodologie d’analyse de performance plus globale appelée Pamda.Nous décrirons aussi les différents apports à l’outil Decan. Sont particulièrement détaillées les techniques de préservation des structures de contrôle du programme,ainsi que l’ajout du support pour les programmes parallèles.Finalement, nous effectuons une étude statistique qui permet de vérifier la possibilité d’utiliser des compteurs d’évènements, autres que le temps d’exécution, comme métriques de comparaison entre les variantes Decan / A crucial step in the process of application performance analysis is the accurate detection of program bottlenecks. A bottleneck is any event which contributes to extend the execution time. Determining their cause is important for application developpers as it enable them to detect code design and generation flaws.Bottleneck detection is becoming a difficult art. Techniques such as event counts,which succeeded to find bottlenecks easily in the past, became less efficient because of the increasing complexity of modern micro-processors, and because of the introduction of parallelism at several levels. Consequently, a real need for new analysis approaches is present in order to face these challenges.Our work focuses on performance analysis and bottleneck detection of computeintensive loops in scientific applications. We work on Decan, a performance analysis and bottleneck detection tool, which offers an interesting and promising approach called Decremental Analysis. The tool, which operates at binary level, is based on the idea of performing controlled modifications on the instructions of a loop, and comparing the new version (called variant) to the original one. The goal is to assess the cost of specific events, and thus the existence or not of bottlenecks.Our first contribution, consists of extending Decan with new variants that we designed, tested and validated. Based on these variants, we developed analysis methods which we used to characterize hot loops and find their bottlenecks. Welater, integrated the tool into a performance analysis methodology (Pamda) which coordinates several analysis tools in order to achieve a more efficient application performance analysis.Second, we introduce several improvements on the Decan tool. Techniquesdeveloped to preserve the control flow of the modified programs, allowed to use thetool on real applications instead of extracted kernels. Support for parallel programs(thread and process based) was also added. Finally, our tool primarily relying on execution time as the main concern for its analysis process, we study the opportunity of also using other hardware generated events, through a study of their stability, precision and overhead

La complexité des CPUs s’est accrue considérablement depuis leurs débuts, introduisant des mécanismes comme le renommage de registres, l’exécution dans le désordre, la vectorisation, les préfetchers et les environnements multi-coeurs pour améliorer les performances avec chaque nouvelle génération de processeurs. Cependant, la difficulté a suivi la même tendance pour ce qui est a) d’utiliser ces mêmes mécanismes à leur plein potentiel, b) d’évaluer si un programme utilise une machine correctement, ou c) de savoir si le design d’un processeur répond bien aux besoins des utilisateurs.Cette thèse porte sur l’amélioration de l’observabilité des facteurs limitants dans les boucles de calcul intensif, ainsi que leurs interactions au sein de microarchitectures modernes.Nous introduirons d’abord un framework combinant CQA et DECAN (des outils d’analyse respectivement statique et dynamique) pour obtenir des métriques détaillées de performance sur des petits codelets et dans divers scénarios d’exécution.Nous présenterons ensuite PAMDA, une méthodologie d’analyse de performance tirant partie de l’analyse de codelets pour détecter d’éventuels problèmes de performance dans des applications de calcul à haute performance et en guider la résolution.Un travail permettant au modèle linéaire Cape de couvrir la microarchitecture Sandy Bridge de façon détaillée sera décrit, lui donnant plus de flexibilité pour effectuer du codesign matériel / logiciel. Il sera mis en pratique dans VP3, un outil évaluant les gains de performance atteignables en vectorisant des boucles.Nous décrirons finalement UFS, une approche combinant analyse statique et simulation au cycle près pour permettre l’estimation rapide du temps d’exécution d’une boucle en prenant en compte certaines des limites de l’exécution en désordre dans des microarchitectures modernes / The complexity of CPUs has increased considerably since their beginnings, introducing mechanisms such as register renaming, out-of-order execution, vectorization,prefetchers and multi-core environments to keep performance rising with each product generation. However, so has the difficulty in making proper use of all these mechanisms, or even evaluating whether one’s program makes good use of a machine,whether users’ needs match a CPU’s design, or, for CPU architects, knowing how each feature really affects customers.This thesis focuses on increasing the observability of potential bottlenecks inHPC computational loops and how they relate to each other in modern microarchitectures.We will first introduce a framework combining CQA and DECAN (respectively static and dynamic analysis tools) to get detailed performance metrics on smallcodelets in various execution scenarios.We will then present PAMDA, a performance analysis methodology leveraging elements obtained from codelet analysis to detect potential performance problems in HPC applications and help resolve them. A work extending the Cape linear model to better cover Sandy Bridge and give it more flexibility for HW/SW codesign purposes will also be described. It will bedirectly used in VP3, a tool evaluating the performance gains vectorizing loops could provide.Finally, we will describe UFS, an approach combining static analysis and cycle accurate simulation to very quickly estimate a loop’s execution time while accounting for out-of-order limitations in modern CPUs

Dans le domaine du calcul de haute performance, les architectures d’exécution sont en continuelle évolution. L’augmentation du nombre de nœuds de calcul, ou le choix d’une topologie réseau plus rapide représentent un investissement important tant en temps qu’en moyen financier. Les méthodes de prédiction de performances permettent de guider ce choix. En parallèle à ce développement, les systèmes HPC pair-à-pair (P2P) se sont également développés ces dernières années. Ce type d’architecture hétérogène permettrait la résolution des problèmes scientifiques pour un coût très faible par rapport au coût d’une architecture dédiée.Ce manuscrit présente une méthode nouvelle de prédiction de performances pour les applications réelles de calcul distribué, exécutées dans des conditions réelles. La prédiction prend en compte l’optimisation du compilateur. Les résultats sont extrapolables et ils sont obtenus pour un ralentissement réduit. Ce travail de recherche est implémenté dans un logiciel nouveau nommé dPerf. dPerf est capable de prédire les performances des applications C, C++ ou Fortran qui communiquent en utilisant les normes MPI ou P2P-SAP et qui s’exécutent sur une architecture cible pair à pair, hétérogène et décentralisée. La précision de cette contribution a été étudiée sur (i) la transformée Laplace, pour l’aspect séquentiel, (ii) le benchmark IS de NAS, pour l’aspect MPI, (iii) et le code de l’obstacle pour l’aspect calcul P2P décentralisé et l’extrapolation du nombre de nœuds. / In the field of high performance computing, the architectures evolve continuously. In order to increase the number of computing nodes or the network speed, an important investment must be considered, from both temporal and financial point of view. Performance prediction methods aim at assisting in finding the best trade-off for such an investment. At the same time, P2P HPC systems have known an increase in development. These heterogeneous architectures would allow solving scientific problems at a low cost, with respect to dedicated systems.The manuscript presents a new method for performance prediction. This method applies to real applications for distributed computing, considered in a real execution environment. This method uses information about the different compiler optimization levels. The prediction results are obtained with reduced slowdown and are scalable. This thesis took shape in the development of the dPerf tool. dPerf predicts the performances of C, C++, and Fortran application, which use MPI or P2P-SAP to communicate. The applications modeled by dPerf are meant for execution on P2P heterogeneous architectures, with a decentralized communication topology. The accuracy of dPerf has been studied on three applications: (i) the Laplace transform, for sequential codes, (ii) the NAS Integer Sort benchmark for distributed MPI programs, (iii) and the obstacle problem, for the decentralized P2P computing and the scaling of the number of computing nodes.

Ce mémoire d'habilitation résume la majeure partie de mes recherches, depuis la fin de mon doctorat, fin 2004, jusqu'à aujourd'hui. Le but essentiel de mes recherches est le développement de méthodes fondées sur des bases mathématiques et performantes en pratique pour s'assurer de la correction des logiciels. J'utilise des approximations pour permettre une bonne performance, tandis que la validité des résultats est garantie par l'emploi exclusif de sur-approximations des ensembles des comportements des programmes. Ma recherche est basée sur l'interprétation abstraite, une théorie très puissante des approximations de sémantiques permettant aisément de les développer, les comparer, les combiner. Je m'emploie en particulier au développement de nouveaux composants réutilisables d'abstraction, les domaines abstraits, qui sont directement implantables en machine, ainsi qu'à leur utilisation au sein d'analyseurs statiques, qui sont des outils de vérification automatique de programmes. Mes premières recherches concernaient l'inférence de propriétés numériques de programmes séquentiels, tandis que mes recherches actuelles se tournent vers l'analyse de programmes concurrents, d'où le titre de ce mémoire. Les deux premiers chapitres de ce mémoire constituent une introduction, tandis que les suivants présentent mon travail d'habilitation proprement dit. Le premier chapitre est une introduction informelle à la problématique de l'analyse de programmes, aux méthodes existantes, leurs forces et leurs faiblesses. Le deuxième chapitre présente de manière formelle les outils dont nous aurons besoin par la suite : les bases de l'interprétation abstraite, quelques domaines abstraits existants et la construction d'analyses statiques par interprétation abstraite, ainsi que quelques résultats utiles que j'ai obtenu en doctorat. Le troisième chapitre est consacré aux aspects spécifiques de l'analyse de programmes concurrents. Cette recherche, très personnelle, a abouti à la construction d'une méthode d'analyse de programmes concurrents, paramétrée par le choix de domaines abstraits, et basée sur une notion d'interférence abstrayant les interactions entre threads. Ainsi, l'analyse construite est modulaire pour les threads. Cette méthode est reliée aux preuves rely-guarantee proposées par Jones, ce que nous montrons formellement dans une première partie. Nous construisons ensuite une analyse à grands pas basée sur les interférences, efficace et facile à implanter. Les deux dernière parties étudient les liens entre l'analyse et les modèles mémoires faiblement cohérents (désormais incontournables) ainsi que le raffinement de l'analyse pour tenir compte des propriétés spécifiques des ordonnanceurs temps-réels (nous étudions en particulier l'effet des priorités des threads et l'emploi d'objets de synchronisation). Le quatrième et le cinquième chapitres sont consacrés à la constructions de domaines abstraits. Ceux-ci ne sont pas spécifiquement liés au problème de la concurrence ; ils sont utiles à l'analyse de tous programmes, séquentiels comme concurrents. Le chapitre 4 étudie des domaines numériques inférant des égalités et inégalités affines, développés en collaboration avec Liqian Chen, alors doctorant en visite à l'ENS. La motivation première était l'emploi de nombres à virgule flottante afin d'améliorer l'efficacité du domaine des polyèdres, mais ces travaux ont également débouché sur la découverte de nouveaux domaines, basés sur les relations affines à coefficients intervalles, que nous présentons également. Le chapitre 5 étudie les abstractions de types de données réalistes, comme ceux rencontrés dans le langage C : les entiers machines, les nombres à virgule flottante, et les blocs structurés (tableaux, structures, unions). Nos abstractions modélisent finement les détails de l'encodage en mémoire des données afin de permettre l'analyse de programmes qui en dépendent (par exemple, ceux utilisant le type-punning). Ces abstractions sont motivées par nos expériences d'analyses, avec les outils Astrée et AstréeA, de programmes C industriels ; ceux-ci employant fréquemment ce type de constructions de bas niveau. Le sixième chapitre est consacré aux applications des méthodes présentées ci-dessus à la construction d'outils d'analyse statique. Il décrit en particulier mon travail sur l'outil Astrée que j'ai co-développé avec l'équipe Abstraction pendant et après mon doctorat, et qui a été industrialisé en 2009. Mes résultats théoriques et appliqués ont contribué au succès d'Astrée, tandis que celui-ci m'a fourni de nouveaux thèmes de recherches, sous la forme de problèmes concrets dont la résolution n'a pu se faire que grâce à des développements théoriques. Ce chapitre décrit également AstréeA, une extension d'Astrée utilisant l'abstraction d'interférences proposée plus haut pour l'analyse de programmes concurrents (Astrée étant limité aux programmes séquentiels). Il décrit également Apron, une bibliothèque de domaines abstraits numériques que j'ai co-développée. Il s'agit d'un outil plus académique, dont le but est d'encourager la recherche sur les domaines numériques abstraits. Le mémoire se conclue par quelques perspectives sur des recherches futures.

Ce mémoire présente une nouvelle approche pour le calcul de temps d'exécution au pire (WCET) de tâche temps-réel critique, en particulier en ce qui concerne les aléas dus aux caches mémoire. Le point général est fait sur la problématique et l'état de l'art en la matière, mais l'accent est mis sur la théorie elle-même et son formalisme, d'abord dans le cadre monotâche puis dans le cadre multitâche. La méthode utilisée repose sur une technique d'interprétation abstraite, comme la plupart des autres méthodes de calcul de WCET, mais le formalisme est dans une approche probabiliste (bien que déterministe dans le cadre monotâche) de par l'utilisation de chaînes de Markov. La généralisation au cadre multitâche utilise les propriétés proba- bilistes pour faire une évaluation pessimiste d'un WCET et d'un écart type au pire, grâce à une modification astucieuse du propagateur dans ce cadre. Des premières évaluations du modèle, codées à la main à partir des résultats de compilation d'applications assez simples montrent des résultats promet- teurs quant à l'application du modèle sur des programmes réels en vraie grandeur.

Cette thèse présente les fondements théoriques et pratiques d'un système pour l'analyse statique de langages manipulant des documents et données XML. Le système s'appuie sur une logique temporelle de point fixe avec programmes inverses, dérivée du mu-calcul modal, dans laquelle les modèles sont des arbres finis. Cette logique est suffisamment expressive pour prendre en compte les langages réguliers d'arbres ainsi que la navigation multidirectionnelle dans les arbres, tout en ayant une complexité simplement exponentielle. Plus précisément, la décidabilité de cette logique est prouvée en temps 2^O(n) où n est la taille de la formule dont le statut de vérité est déterminé.<br /><br />Les principaux concepts de XML sont traduits linéairement dans cette logique. Ces concepts incluent la navigation et la sémantique de sélection de noeuds du langage de requêtes XPath, ainsi que les langages de schémas (incluant DTD et XML Schema). Grâce à ces traductions, les problèmes d'importance majeure dans les applications XML sont réduits à la satisfaisabilité de la logique. Ces problèmes incluent notamment l'inclusion, la satisfaisabilité, l'équivalence, l'intersection, le recouvrement des requêtes, en présence ou en l'absence de contraintes régulières d'arbres, et le typage statique d'une requête annotée.<br /><br />Un algorithme correct et complet pour décider la logique est proposé, accompagné d'une analyse détaillée de sa complexité computationnelle, et des techniques d'implantation cruciales pour la réalisation d'un solveur efficace en pratique. Des expérimentations avec l'implantation complète du système sont présentées. Le système apparaît efficace et utilisable en pratique sur plusieurs scénarios réalistes.<br /><br />La principale application de ce travail est une nouvelle classe d'analyseurs statiques pour les langages de programmation utilisant des requêtes XPath et des types réguliers d'arbres. De tels analyseurs permettent de s'assurer, au moment de la compilation, de propriétés importantes comme le typage correct des programmes ou leur optimisation, pour un traitement plus sûr et plus efficace des données XML.