L’objectif général de cette thèse est le développement de méthodes mathématiques correctes et efficaces en pratique pour prouver automatiquement la correction de logiciels. Plus précisément, cette thèse est fondée sur la théorie de l’interprétation abstraite, un cadre mathématique puissant pour l’approximation du comportement des programmes. En particulier, cette thèse se concentre sur la preuve des propriétés de vivacité des programmes, qui représentent des conditions qui doivent être réalisés ultimement ou de manière répétée pendant l’exécution du programme. La terminaison des programmes est la propriété de vivacité la plus fréquemment considérée. Cette thèse conçoit des nouvelles approximations, afin de déduire automatiquement des conditions suffisantes pour la terminaison des programmes et synthétiser des fonctions de rang définies par morceaux, qui fournissent des bornes supérieures sur le temps d’attente avant la terminaison. Les approximations sont paramétriques dans le choix entre l’expressivité et le coût des approximations sous-jacentes, qui maintiennent des informations sur l’ensemble des valeurs possibles des variables du programme ainsi que les relations numériques possibles entre elles. Cette thèse développe également un cadre d’interprétation abstraite pour prouver des propriétés de vivacité, qui vient comme une généralisation du cadre proposé pour la terminaison. En particulier, le cadre est dédié à des propriétés de vivacité exprimées dans la logique temporelle, qui sont utilisées pour s’assurer qu’un événement souhaitable se produit une fois ou une infinité de fois au cours de l’exécution du programme. Comme pour la terminaison,des fonctions de rang définies par morceaux sont utilisées pour déduire des préconditions suffisantes pour ces propriétés, et fournir des bornes supérieures sur le temps d’attente avant un événement souhaitable. Les résultats présentés dans cette thèse ont été mis en œuvre dans un prototype d’analyseur. Les résultats expérimentaux montrent qu’il donne de bons résultats sur une grande variété de programmes, il est compétitif avec l’état de l’art, et il est capable d’analyser des programmes qui sont hors de la portée des méthodes existantes. / The overall aim of this thesis is the development of mathematically sound and practically efficient methods for automatically proving the correctness of computer software. More specifically, this thesis is grounded in the theory of abstract interpretation, a powerful mathematical framework for approximating the behavior of programs. In particular, this thesis focuses on provingprogram liveness properties, which represent requirements that must be eventually or repeatedly realized during program execution. Program termination is the most prominent liveness property. This thesis designs new program approximations, in order to automatically infer sufficient preconditions for program termination and synthesize so called piecewisedefined ranking functions, which provide upper bounds on the waiting time before termination. The approximations are parametric in the choice between the expressivity and the cost of the underlying approximations, which maintain information about the set of possible values of the program variables along with the possible numerical relationships between them. This thesis also contributes an abstract interpretation framework for proving liveness properties, which comes as a generalization of the framework proposedfor termination. In particular, the framework is dedicated to liveness properties expressed in temporal logic, which are used to ensure that some desirable event happens once or infinitely many times during program execution. As for program termination, piecewise-defined ranking functions are used to infer sufficient preconditions for these properties, and to provide upper boundson the waiting time before a desirable event. The results presented in this thesis have been implemented into a prototype analyzer. Experimental results show that it performs well on a wide variety of benchmarks, it is competitive with the state of the art, and is able to analyze programs that are out of the reach of existing methods.

Les logiciels critiques nécessitent l’obtention d’une évaluation de conformité aux normesen vigueur avant leur mise en service. Cette évaluation est obtenue après un long travaild’analyse effectué par les évaluateurs de logiciels critiques. Ces derniers peuvent être aidéspar des outils utilisés de manière interactive pour construire des modèles, en faisant appel àdes analyses de flots d’information. Des outils comme SPARK-Ada existent pour des sous-ensembles du langage Ada utilisés pour le développement de logiciels critiques. Cependant,des langages émergents comme ceux de la famille ML ne disposent pas de tels outils adaptés.La construction d’outils similaires pour les langages ML demande une attention particulièresur certaines spécificités comme les fonctions d’ordre supérieur ou le filtrage par motifs. Cetravail présente une analyse de flot d’information pour de tels langages, spécialement conçuepour répondre aux besoins des évaluateurs. Cette analyse statique prend la forme d’uneinterprétation abstraite de la sémantique opérationnelle préalablement enrichie par desinformations de dépendances. Elle est prouvée correcte vis-à-vis d’une définition formellede la notion de dépendance, à l’aide de l’assistant à la preuve Coq. Ce travail constitue unebase théorique solide utilisable pour construire un outil efficace pour l’analyse de toléranceaux pannes. / Critical software needs to obtain an assessment before commissioning in order to ensure compliance tostandards. This assessment is given after a long task of software analysis performed by assessors. Theymay be helped by tools, used interactively, to build models using information-flow analysis. Tools likeSPARK-Ada exist for Ada subsets used for critical software. But some emergent languages such as thoseof the ML family lack such adapted tools. Providing similar tools for ML languages requires specialattention on specific features such as higher-order functions and pattern-matching. This work presentsan information-flow analysis for such a language specifically designed according to the needs of assessors.This analysis is built as an abstract interpretation of the operational semantics enriched with dependencyinformation. It is proved correct according to a formal definition of the notion of dependency using theCoq proof assistant. This work gives a strong theoretical basis for building an efficient tool for faulttolerance analysis.

La validation des logiciels est une partie cruciale dans le cycle de leur développement. Deux techniques de vérification et de validation se sont démarquées au cours de ces dernières années : l’analyse statique et l’analyse dynamique. Les points forts et faibles des deux techniques sont complémentaires. Nous présentons dans cette thèse une combinaison originale de ces deux techniques. Dans cette combinaison, l’analyse statique signale les instructions risquant de provoquer des erreurs à l’exécution, par des alarmes dont certaines peuvent être de fausses alarmes, puis l’analyse dynamique (génération de tests) est utilisée pour confirmer ou rejeter ces alarmes. L’objectif de cette thèse est de rendre la recherche d’erreurs automatique, plus précise, et plus efficace en temps. Appliquée à des programmes de grande taille, la génération de tests, peut manquer de temps ou d’espace mémoire avant de confirmer certaines alarmes comme de vraies erreurs ou conclure qu’aucun chemin d’exécution ne peut atteindre l’état d’erreur de certaines alarmes et donc rejeter ces alarmes. Pour surmonter ce problème, nous proposons de réduire la taille du code source par le slicing avant de lancer la génération de tests. Le slicing transforme un programme en un autre programme plus simple, appelé slice, qui est équivalent au programme initial par rapport à certains critères. Quatre utilisations du slicing sont étudiées. La première utilisation est nommée all. Elle consiste à appliquer le slicing une seule fois, le critère de simplification étant l’ensemble de toutes les alarmes du programme qui ont été détectées par l’analyse statique. L’inconvénient de cette utilisation est que la génération de tests peut manquer de temps ou d’espace et les alarmes les plus faciles à classer sont pénalisées par l’analyse d’autres alarmes plus complexes. Dans la deuxième utilisation, nommée each, le slicing est effectué séparément par rapport à chaque alarme. Cependant, la génération de tests est exécutée pour chaque programme et il y a un risque de redondance d’analyse si des alarmes sont incluses dans d’autres slices. Pour pallier ces inconvénients, nous avons étudié les dépendances entre les alarmes et nous avons introduit deux utilisations avancées du slicing, nommées min et smart, qui exploitent ces dépendances. Dans l’utilisation min, le slicing est effectué par rapport à un ensemble minimal de sous-ensembles d’alarmes. Ces sous-ensembles sont choisis en fonction de dépendances entre les alarmes et l’union de ces sous-ensembles couvre l’ensemble de toutes les alarmes. Avec cette utilisation, on a moins de slices qu’avec each, et des slices plus simples qu’avec all. Cependant, l’analyse dynamique de certaines slices peut manquer de temps ou d’espace avant de classer certaines alarmes, tandis que l’analyse dynamique d’une slice éventuellement plus simple permettrait de les classer. L’utilisation smart consiste à appliquer l’utilisation précédente itérativement en réduisant la taille des sous-ensembles quand c’est nécessaire. Lorsqu’une alarme ne peut pas être classée par l’analyse dynamique d’une slice, des slices plus simples sont calculées. Nous prouvons la correction de la méthode proposée. Ces travaux sont implantés dans sante, notre outil qui relie l’outil de génération de tests PathCrawler et la plate-forme d’analyse statique Frama-C. Des expérimentations ont montré, d’une part, que notre combinaison est plus performante que chaque technique utilisée indépendamment et, d’autre part, que la vérification devient plus rapide avec l’utilisation du slicing. De plus, la simplification du programme par le slicing rend les erreurs détectées et les alarmes restantes plus faciles à analyser / Software validation remains a crucial part in software development process. Two major techniques have improved in recent years, dynamic and static analysis. They have complementary strengths and weaknesses. We present in this thesis a new original combination of these methods to make the research of runtime errors more accurate, automatic and reduce the number of false alarms. We prove as well the correction of the method. In this combination, static analysis reports alarms of runtime errors some of which may be false alarms, and test generation is used to confirm or reject these alarms. When applied on large programs, test generation may lack time or space before confirming out certain alarms as real bugs or finding that some alarms are unreachable. To overcome this problem, we propose to reduce the source code by program slicing before running test generation. Program slicing transforms a program into another simpler program, which is equivalent to the original program with respect to certain criterion. Four usages of program slicing were studied. The first usage is called all. It applies the slicing only once, the simplification criterion is the set of all alarms in the program. The disadvantage of this usage is that test generation may lack time or space and alarms that are easier to classify are penalized by the analysis of other more complex alarms. In the second usage, called each, program slicing is performed with respect to each alarm separately. However, test generation is executed for each sliced program and there is a risk of redundancy if some alarms are included in many slices. To overcome these drawbacks, we studied dependencies between alarms on which we base to introduce two advanced usages of program slicing : min and smart. In the min usage, the slicing is performed with respect to subsets of alarms. These subsets are selected based on dependencies between alarms and the union of these subsets cover the whole set of alarms. With this usage, we analyze less slices than with each, and simpler slices than with all. However, the dynamic analysis of some slices may lack time or space before classifying some alarms, while the dynamic analysis of a simpler slice could possibly classify some. Usage smart applies previous usage iteratively by reducing the size of the subsets when necessary. When an alarm cannot be classified by the dynamic analysis of a slice, simpler slices are calculated. These works are implemented in sante, our tool that combines the test generation tool PathCrawler and the platform of static analysis Frama-C. Experiments have shown, firstly, that our combination is more effective than each technique used separately and, secondly, that the verification is faster after reducing the code with program slicing. Simplifying the program by program slicing also makes the detected errors and the remaining alarms easier to analyze

Sur des architectures récentes, un programme numérique peut donner des réponses différentes en fonction du hardware et du compilateur. Ces incohérences des résultats viennent du fait que chaque calcul en virgule flottante est effectué avec des précisions différentes. Le but de cette thèse est de prouver formellement des propriétés des programmes opérant sur des nombres flottants en prenant en compte l’architecture et le compilateur. Pour le faire, nous avons proposé deux approches différentes. La première approche est de prouver des propriétés des programmes en virgule flottante qui sont vraies sur plusieurs architectures et compilateurs. Cette approche ne considère que les erreurs d’arrondi qui doivent être validées quels que soient l’environnement matériel et le choix du compilateur. Elle est implantée dans la plate-forme Frama-C pour l’analyse statique de code C. La deuxième approche consiste à prouver des propriétés des programmes en analysant leur code assembleur. Nous nous concentrons sur des problèmes et des pièges qui apparaissent sur des calculs en virgule flottante. L’analyse directe du code assembleur nous permet de considérer des caratéristiques dépendant de l’architecture ou du compilateur telle que l’utilisation des registres en précision étendue. Cette approche est implantée comme une sur-couche de la plate-forme Why pour la vérification déductive. / On some recently developed architectures, a numerical program may give different answers depending on the execution hardware and the compilation. These discrepancies of the results come from the fact that each floating-point computation is calculated with different precisions. The goal of this thesis is to formally prove properties about numerical programs while taking the architecture and the compiler into account. In order to do that, we propose two different approaches. The first approach is to prove properties of floating-point programs that are true for multiple architectures and compilers. This approach states the rounding error of each floating-point computation whatever the environment and the compiler choices. It is implemented in the Frama-C platform for static analysis of C code. The second approach is to prove behavioral properties of numerical programs by analyzing their compiled assembly code. We focus on the issues and traps that may arise on floating-point computations. Direct analysis of the assembly code allows us to take into account architecture- or compiler-dependent features such as the possible use of extended precision registers. It is implemented above the Why platform for deductive verification

L’analyse comportementale traditionnelle opère en général au niveau de l’implantation de comportements malveillants. Pourtant, elle s’intéresse surtout à l’identification de fonctionnalités données et elle se situe donc plus naturellement à un niveau fonctionnel. Dans cette thèse, nous définissons une forme d’analyse comportementale de programmes qui opère non pas sur les interactions élémentaires d’un programme avec le système mais sur la fonction que le programme réalise. Cette fonction est extraite des traces d’un pro- gramme, un procédé que nous appelons abstraction. Nous définissons de façon simple, intuitive et formelle les fonctionnalités de base à abstraire et les comportements à détecter, puis nous proposons un mécanisme d’abstraction applicable à un cadre d’analyse statique ou dynamique, avec des algorithmes pratiques à complexité raisonnable, enfin nous décrivons une technique d’analyse comportementale intégrant ce mécanisme d’abstraction. Notre méthode est particulièrement adaptée à l’analyse des programmes dans des langages de haut niveau ou dont le code source est connu, pour lesquels l’analyse statique est facilitée : applications mobiles en .NET ou Java, scripts, extensions de navigateurs, composants off-the-shelf.Le formalisme d’analyse comportementale par abstraction que nous proposons repose sur la théorie de la réécriture de mots et de termes, les langages réguliers de mots et de termes et le model checking. Il permet d’identifier efficacement des fonctionnalités dans des traces et ainsi d’obtenir une représentation des traces à un niveau fonctionnel; il définit les fonctionnalités et les comportements de façon naturelle, à l’aide de formules de logique temporelle, ce qui garantit leur simplicité et leur flexibilité et permet l’utilisation de techniques de model checking pour la détection de ces comportements ; il opère sur un ensemble quelconque de traces d’exécution ; il prend en compte le flux de données dans les traces d’exécution; et il permet, sans perte d’efficacité, de tenir compte de l’incertitude dans l’identification des fonctionnalités. Un cadre d’expérimentation a été mis en place dans un contexte d’analyse dynamique comme statique / Traditional behavior analysis usually operates at the implementation level of malicious behaviors. Yet, it is mostly concerned with the identification of given functionalities and is therefore more naturally defined at a functional level. In this thesis, we define a form of program behavior analysis which operates on the function realized by a program rather than on its elementary interactions with the system. This function is extracted from program traces, a process we call abstraction. We define in a simple, intuitive and formal way the basic functionalities to abstract and the behaviors to detect, then we propose an abstraction mechanism applicable both to a static or to a dynamic analysis setting, with practical algorithms of reasonable complexity, finally we describe a behavior analysis technique integrating this abstraction mechanism. Our method is particularly suited to the analysis of programs written in high level languages or with a known source code, for which static analysis is facilitated: mobile applications for .NET or Java, scripts, browser addons, off-the-shelf components.The formalism we propose for behavior analysis by abstraction relies on the theory of string and terms rewriting, word and tree languages and model checking. It allows an efficient identification of functionalities in traces and thus the construction of a represen- tation of traces at a functional level; it defines functionalities and behaviors in a natural way, using temporal logic formulas, which assure their simplicity and their flexibility and enables the use of model checking techniques for behavior detection; it operates on an unrestricted set of execution traces; it handles the data flow in execution traces; and it allows the consideration of uncertainty in the identification of functionalities, with no complexity overhead. Experiments have been conducted in a dynamic and static analysis setting

Les tâches critiques en systèmes temps-réel sont soumises à des contraintes temporelles et de correction. La validation d'un tel système repose sur l'estimation du comportement temporel au pire cas de ses tâches. Le partage de ressources, inhérent aux architectures multi-cœurs, entrave le calcul de ces estimations. Le comportement temporel d'une tâche dépend de ses rivales du fait de l'arbitrage de l'accès aux ressources ou de modifications concurrentes de leur état. Cette étude vise à l'estimation de la contribution temporelle de la hiérarchie mémoire au pire temps d'exécution de tâches critiques. Les méthodes existantes, pour caches d'instructions, sont étendues afin de supporter caches de données privés et partagés, et permettre l'analyse de hiérarchies mémoires riches. Le court-circuitage de cache est ensuite utilisé pour réduire la pression sur les caches partagés. Nous proposons à cette fin différentes heuristiques basées sur la capture de la réutilisation de blocs de cache entre différents accès mémoire. Notre seconde proposition est la politique de partitionnement Preti qui permet l'allocation d'un espace sans conflits à une tâche. Preti favorise aussi les performances de tâches non critiques concurrentes aux temps-réel dans les systèmes de criticité hybride. / Critical tasks in the context of real-time systems submit to both timing and correctness constraints. Whence, the validation of a real-time system rely on the estimation of its tasks’ Worst case execution times. Resource sharing, as it occurs on multicore architectures, hinders the computation of such estimates. The timing behaviour of a task is impacted by its concurrents, whether because of resource access arbitration or concurrent modifications of a resource state. This study focuses on estimating the contribution of the memory hierarchy to tasks’ worst case execution time. Existing analysis methods, defined for instruction caches, are extended to support private and shared data caches, hence allowing for the analysis of rich memory hierarchies. Cache bypass is then used to reduce the pressure laid by concurrent tasks on shared caches levels. We propose different bypass heuristics, based on the capture of cache blocks’ reuse between memory accesses. Our second proposal is the Preti partitioning scheme which allows for the allocation to tasks of a cache space, free from inter-task conflicts. Preti offers the added benefit of providing for average-case performance to non-critical tasks concurrent to real-time ones on hybrid criticality systems.

Le but de ce travail est de développer des outils par éléments finis permettant de calculer des structures sandwich sans ajouter aucune autre hypothèse que celle, très générale, de l'élasticité linéaire. Deux voies ont été suivies dans ce travail. Tout d'abord, nous exposons comment développer des éléments finis hybrides, dans lesquels les contraintes aux interfaces entre les différentes couches sont obtenues par l'intermédiaire de multiplicateurs de Lagrange. Des éléments 2D et 3D, basés sur le principe du travail virtuel et sur la fonctionnelle de Pian et Tong sont développés et validés. Ensuite, après avoir examiné les possibilités offertes par le code de calcul Ansys 5.3, nous proposons une méthode de post-traitement, basée sur la fonctionnelle de Reissner, permettant de recouvrer les contraintes d'interfaces à partir des déplacements nodaux obtenus à partir des éléments en déplacements. Finalement ces deux approches sont confrontées entre elles, tant sur le plan de la qualité des résultats numériques que sur la facilité d'utilisation, de programmation et d'implémentation dans des codes de calculs existants.

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.

L'inclusion de requête est un problème bien étudié durant plusieurs décen- nies de recherche. En règle générale, il est défini comme le problème de déterminer si le résultat d'une requête est inclus dans le résultat d'une autre requête pour tout ensem- ble de données. Elle a des applications importantes dans l'optimisation des requêtes et la vérification de bases de connaissances. L'objectif principal de cette thèse est de fournir des procédures correctes et complètes pour déterminer l'inclusion des requêtes SPARQL en vertu d'axiomes exprimés en logiques de description. De plus, nous met- tons en œuvre ces procédures à l'appui des résultats théoriques par l'expérimentation. À ce jour, l'inclusion de requête a été testée à l'aide de différentes techniques: ho- momorphisme de graphes, bases de données canoniques, les techniques de la théorie des automates et réduction au problème de la validité d'une logique. Dans cette thèse, nous utilisons la derniere technique pour tester l'inclusion des requêtes SPARQL utilisant une logique expressive appelée le μ-calcul. Pour ce faire, les graphes RDF sont codés comme des systèmes de transitions, et les requêtes et les axiomes du schéma sont codés comme des formules de μ-calcul. Ainsi, l'inclusion de requêtes peut être réduite au test de la validité d'une formule logique. Dans cette thèse j'identifier les divers fragments de SPARQL (et PSPARQL) et les langages de description logique de schéma pour lequelle l'inculsion est décidable. En outre, afin de fournir théoriquement et expérimentalement des procédures éprouvées pour vérifier l'inclusion de ces fragments décidables. Enfin, cette thèse propose un point de repère pour les solveurs d'inclusion. Ce benchmark est utilisé pour tester et comparer l'état actuel des solveurs d'inclusion.

Afin de pouvoir répondre au mieux aux différents appels d'offres, les constructeurs de grappe de calcul ont besoin d'outils et de méthodes permettant d'aider au mieux la prise de décisions en terme de design architectural. Nos travaux se sont donc intéressés à l'estimation des temps de calcul et à l'étude de la congestion sur le réseau InfiniBand. Ces deux problèmes sont souvent abordés de manière globale. Néanmoins, une approche globale ne permet pas de comprendre les raisons des pertes de performance liées aux choix architecturaux. Notre approche s'est donc orientée vers une étude plus fine. Pour évaluer les temps de calcul, la démarche proposée s'appuie sur une analyse statique ou semistatique du code source afin de le découper en blocs, avant d'effectuer un micro-benchmarking de ces blocs sur l'architecture cible. Pour l'estimation des temps de communication, un modèle de répartition de bande passante pour le réseau InfiniBand a été développé, permettant ainsi de prédire l'impact lié aux communications concurrentes. Ce modèle a ensuite été intégré dans un simulateur pour être validé sur un ensemble de graphes de communication synthétiques et sur l'application Socorro.