Cette thèse s'inscrit dans le domaine de la vérification formelle de programmes parallèles. L'enjeu de la vérification formelle est de s'assurer qu'un programme va bien fonctionner comme il le devrait, sans commettre d'erreur, se bloquer, ou se terminer anormalement. Cela est d'autant plus important dans le domaine du calcul parallèle, où le coût des calculs est parfois très élevé. Le modèle BSP (Bulk Synchronous Parallelism) est un modèle de parallélisme bien adapté à l'utilisation des méthodes formelles. Il garantit une forme de structure dans le programme parallèle, en l'organisant en super-étapes où chacune d'entre elle est composées d'une phase de calculs, puis d'une phase de communications entre les unités de calculs. Dans cette thèse, nous avons choisi d'étendre un outil actuel pour l'adapter à la preuve de programmes BSP. Nous nous sommes basés sur Why, un VCG (générateur de condition de vérification) qui a l'avantage de pouvoir s'interfacer avec plusieurs prouveurs automatiques et assistants de preuve pour décharger les obligations de preuves. Les contributions de cette thèse sont multiples. Dans un premier temps, nous présentons une comparaison des différentes librairies BSP disponibles, afin de mettre en évidence les primitives de programmation BSP les plus utilisées, donc les plus intéressantes à formaliser. Nous présentons ensuite BSP-Why, notre outil de preuve des programmes BSP. Cet outil se repose sur une génération d'un programme séquentiel qui simule le programme parallèle entré permettant ainsi d'utiliser Why et les nombreux prouveurs automatiques associés pour prouver les obligations de preuves. Nous montrons ensuite comment BSP-Why peut-être utilisé pour prouver la correction de quelques algorithmes BSP simples, mais aussi pour un exemple plus complexe qu'est la construction distribuée de l'espace d'états (model-checking) de systèmes et plus particulièrement dans les protocoles de sécurité. Enfin, afin de garantir la plus grande confiance dans l'outil BSP-Why, nous formalisons les sémantiques du langage, dans l'assistant de preuve Coq. Nous démontrons également la correction de la transformation utilisée pour passer d'un programme parallèle à un programme séquentiel / This thesis takes part in the formal verification of parallel programs. The aim of formal verification is to ensure that a program will run as it should, without making mistakes, blocking, or terminating abnormally. This is even more important in the parallel computation field, where the cost of calculations can be very high. The BSP model (Bulk Synchronous Parallelism) is a model of parallelism well suited for the use of formal methods. It guarantees a structure in the parallel program, by organising it into super-steps, each of them consisting of a phase of computations, then communications between the processes. In this thesis, we chose to extend an existing tool to adapt it for the proof of BSP programs. We based ourselves on Why, a VCG (verification condition generator) that has the advantage of being able to interface with several automatic provers and proof assistants to discharge the proof obligations. There are multiple contributions in this thesis. In a first part, we present a comparison of the existing BSP libraries, in order to show the most used BSP primitives, which are the most interesting to formalise. We then present BSP-Why, our tool for the proof of BSP programs. This tools uses a generation of a sequential program to simulate the parallel program in input, thus allowing the use of Why and the numerous associated provers to prove the proof obligations. We then show how BSP-Why can be used to prove the correctness of some basic BSP algorithms, and also on a more complex example, the generation of the state-space (model-checking) of systems, especially for security protocols. Finally, in order to ensure the greatest confidence in the BSP-Why tool, we give a formalisation of the language semantics, in the Coq proof assistant. We also prove the correctness of the transformation used to go from a parallel program to a sequential program

Cette thèse se place dans le cadre des méthodes formelles et plus précisément dans celui de la vérification déductive et du système Why3. Ce dernier fournit un ensemble d'outils pour la spécification, l'implémentation et la vérification à l'aide de démonstrateurs externes. Why3 propose en particulier un langage de programmation adapté à la preuve, appelé WhyML. Un aspect important de ce langage est le code fantôme, à savoir des éléments de programme introduits exclusivement pour les besoins de la spécification et de la preuve. Pour obtenir un code exécutable, le code fantôme est éliminé par un processus automatique appelé extraction. L'une des contributions principales de cette thèse est la formalisation et l'implémentation du mécanisme d'extraction deWhy3. La formalisation consiste à montrer que le programme extrait préserve la sémantique du programme de départ, en s'appuyant notamment sur un système de types avec effets. Ce mécanisme d'extraction a été utilisé avec succès pour obtenir plusieurs modules OCaml corrects par construction, dans le cadre d'une bibliothèque vérifiée de structures de données et d'algorithmes. Cet effort de preuve a conduit à deux autres contributions de cette thèse.La première est une technique systématique pour la vérification de structures avec pointeurs, à l'aide de modèles du tas délimités.Une preuve entièrement automatique d'une structure union-find a pu être obtenue grâce à cette technique. La seconde contribution est un moyen de spécifier un algorithme d'itération indépendamment de son implémentation. Plusieurs curseurs et itérateurs d'ordre supérieur ont été spécifiés et vérifiés en utilisant cette approche. / This thesis is set in the field of formal methods, more precisely in the domain of deductive program verification. Our working context is the Why3 framework, a set of tools to implement, formally specify, and prove programs usingoff-the-shelf theorem provers. Why3 features a programming language,called WhyML, designed with verification in mind. An important feature of WhyML is ghost code: portions of the program that are introduced for the sole purpose of specification andverification. When it comes to get an executable implementation, ghost code is removed by an automatic process called extraction. One of the main contributions of this thesis is the formalization and implementation of Why3's extraction. The formalization consists in showing that the extracted program preserves the same operational behavior as the original source code, based on a type and effect system. The new extraction mechanism has been successfully used to get correct-by-construction OCaml modules, which are part of averified OCaml library of data structures and algorithms. This verification effort led to two other contributions of this thesis.The first is a systematic approach to the verification ofpointer-based data structures using ghost models of fragments of the heap. A fully automatic verification of a union-find data structure was achieved using this technique. The second contribution is a modular way to reason about iteration, independently of the underlying implementation. Several cursors and higher-orderiterators have been specified and verified with this approach.

Cette thèse se positionne dans le domaine de la vérification déductive de programmes, qui consiste à transformer une propriété à vérifier sur un programme en un énoncé logique, pour ensuite démontrer cet énoncé. La vérification effective d'un programme peut poser de nombreuses difficultés pratiques. En fait, les concepts mis en jeu derrière le programme peuvent suffire à faire obstacle à la vérification. En effet, certains programmes peuvent être assez courts et n'utiliser que des constructions simples, et pourtant s'avérer très difficiles à vérifier. Cela nous amène à la question suivante: dans le contexte d'un environnement de vérification déductive de programmes basé sur les démonstrateurs automatiques, quelles méthodes appliquer pour réduire l'effort nécessaire à la fois pour spécifier des comportements attendus complexes, ainsi que pour démontrer qu'un programme respecte ces comportements attendus? Pour mener notre étude, nous nous sommes placés dans le cadre de l'environnement de vérification déductive de programmes Why3. La vérification de programmes en Why3 est basée sur la génération de conditions de vérification, et l'usage de démonstrateurs externes pour les prouver, que ces démonstrateurs soient automatiques ou interactifs. Nous avons développé plusieurs méthodes, certaines générales et d'autres spécifiques à des classes de programmes, pour réduire l'effort manuel. Nos contributions sont les suivantes. Tout d'abord, nous ajoutons des fonctionnalités à Why3 pour assister le processus de vérification, notamment un mécanisme léger de preuve déclarative basé sur la notion d'indicateurs de coupures. Ensuite, nous présentons une méthode de vérification d'absence de débordement arithmétique pour une classe d'utilisation des entiers difficile à traiter par les méthodes standards. Enfin, nous nous intéressons au développement d'une bibliothèque générique pour la spécification et la preuve de programmes générateurs de code. / This thesis is set in the domain of deductive verification of programs, which consists of transforming a property to be verified about a program into a logical statement, and then proving this statement. Effective verification of a program can pose many practical difficulties. In fact, the concepts behind the program may be sufficient to impede verification. Indeed, some programs can be quite short and use only simple constructions, and yet prove very difficult to verify. This leads us to the following question: in the context of a deductive program verification environment based on automatic provers, what methods can be applied to reduce the effort required both to specify complex behaviors, as well as to prove that a program respects these expected behaviors? To carry out our study, we placed ourselves in the context of the deductive verification environment of programs Why3. The verification of programs in Why3 is based on the generation of verification conditions, and the use of external provers to prove them, whether these provers are automatic or interactive. We have developed several methods, some general and others specific to some program classes, to reduce manual effort. Our contributions are as follows. First, we add features to Why3 to assist the verification process, including a lightweight declarative proof mechanism based on the notion of cut indicators. Then we present a method for checking the absence of arithmetic overflow, for use cases which are difficult to process by standard methods. Finally, we are interested in the development of a generic library for the specification and proof of code generating programs.

La vérification déductive de programmes consiste à annoter des programmes par une spécification, c'est-à-dire un ensemble de formules logiques décrivant le comportement du programme, et à prouver que les programmes vérifient bien leur spécification. Des outils tels que la plate-forme Why prennent en entrée un programme et sa spécification et calculent des formules logiques telles que, si elles sont prouvées, le programme vérifie sa spécification. Ces formules logiques peuvent être prouvées automatiquement ou à l'aide d'assistants de preuve.Lorsqu'un programme est écrit dans un langage supportant les alias de pointeurs, c'est-à-dire si plusieurs variables peuvent désigner la même case mémoire, alors le raisonnement sur le programme devient particulièrement ardu. Il est nécessaire de spécifier quels pointeurs peuvent être égaux ou non. Les invariants des structures de données, en particulier, sont plus difficiles à vérifier.Cette thèse propose un système de type permettant de structurer la mémoire de façon modulaire afin de contrôler les alias de pointeurs et les invariants de données. Il est basé sur les notions de région et de permission. Les programmes sont ensuite interprétés vers Why de telle façon que les pointeurs soient séparés au mieux, facilitant ainsi le raisonnement. Cette thèse propose aussi un mécanisme d'inférence permettant d'alléger le travail d'annotation des opérations de régions introduites par le langage. Un modèle est introduit pour décrire la sémantique du langage et prouver sa sûreté. En particulier, il est prouvé que si le type d'un pointeur affirme que celui-ci vérifie son invariant, alors cet invariant est effectivement vérifié dans le modèle. Cette thèse a fait l'objet d'une implémentation sous la forme d'un outil nommé Capucine. Plusieurs exemples ont été écrits pour illustrer le langage, et ont été vérifié à l'aide de Capucine.

Cette thèse se place dans le contexte de la vérification déductive des programmes et a pour objectif de formaliser un certain nombre de concepts qui sont mis en œuvre dans l'outil de vérification Why3.L'idée générale est d'explorer des solutions qu'une approche à base de systèmes de types peut apporter à la vérification. Nous commençons par nous intéresser à la notion du code fantôme, une technique implantée dans de nombreux outils de vérification modernes, qui consiste à donner à des éléments de la spécification les apparences d'un code opérationnel. L'utilisation correcte du code fantôme requiert maintes précautions puisqu'il ne doit jamais interférer avec le reste du code. Le premier chapitre est consacré à une formalisation du code fantôme, en illustrant comment un système de types avec effets en permet une utilisation à la fois correcte et expressive. Puis nous nous intéressons à la vérification des programmes manipulant des pointeurs. En présence d'aliasing, c'est-à-dire lorsque plusieurs pointeurs manipulés dans un programme dénotent une même case mémoire, la spécification et la vérification deviennent non triviales. Plutôt que de nous diriger vers des approches existantes qui abordent le problème d'aliasing dans toute sa complexité, mais sortent du cadre de la logique de Hoare, nous présentons un système de types avec effets et régions singletons qui permet d'effectuer un contrôle statique des alias avant même de générer les obligations de preuve. Bien que ce système de types nous limite à des pointeurs dont l'identité peut être connue statiquement, notre observation est qu'il convient à une grande majorité des programmes que l'on souhaite vérifier. Enfin, nous abordons les questions liées à la vérification de programmes conçus de façon modulaire. Concrètement, nous nous intéressons à une situation où il existe une barrière d'abstraction entre le code de l'utilisateur et celui des bibliothèques dont il dépend. Cela signifie que les bibliothèques fournissent à l'utilisateur une énumération de fonctions et de structures de données manipulées, sans révéler les détails de leur implémentation. Le code de l'utilisateur ne peut alors exploiter ces données qu'à travers un ensemble de fonctions fournies. Dans une telle situation, la vérification peut elle-même être modulaire. Du côté de l'utilisateur, la vérification ne doit alors s'appuyer que sur des invariants de type et des contrats de fonctions exposés par les bibliothèques. Du côté de ces dernières, la vérification doit garantir que la représentation concrète raffine correctement les entités exposées, c'est-à-dire en préservant les invariants de types et les contrats de fonctions. Dans le troisième chapitre nous explorons comment un système de types permettant le contrôle statique des alias peut être adapté à la vérification modulaire et le raffinement des structures de données. / This thesis is conducted in the framework of deductive software verification.is aims to formalize some concepts that are implemented in the verification tool Why3. The main idea is to explore solutions that a type system based approach can bring to deductive verification. First, we focus our attention on the notion of ghost code, a technique that is used in most of modern verification tools and which consists in giving to some parts of specification the appearance of operational code. Using ghost code correctly requires various precautions since the ghost code must never interfere with the operational code. The first chapter presents a type system with effects illustrating how ghost code can be used in a way which is both correct and expressive. The second chapter addresses some questions related to verification of programs with pointers in the presence of aliasing, i.e. when several pointers handled by a program denote a same memory cell. Rather than moving towards to approaches that address the problem in all its complexity to the costs of abandoning the framework of Hoare logic, we present a type system with effects and singleton regions which resolves a liasing issues by performing a static control of aliases even before the proof obligations are generated. Although our system is limited to pointers whose identity must be known statically, we observe that it fits for most of the code we want to verify. Finally, we focus our attention on a situation where there exists an abstraction barrier between the user's code and the one of the libraries which it depends on. That means that libraries provide the user a set of functions and of data structures, without revealing details of their implementation. When programs are developed in a such modular way, verification must be modular it self. It means that the verification of user's code must take into account only function contracts supplied by libraries while the verification of libraries must ensure that their implementations refine correctly the exposed entities. The third chapter extends the system presented in the previous chapter with these concepts of modularity and data refinement.

Le but de cette thèse est de spécifier et prouver des programmes avec pointeurs, tels que des programmes C, en utilisant des techniques de raffinement. L'approche proposée permet de faire un compromis entre les techniques complexes qui existent dans la littérature et ce qui est utilisable dans l'industrie, en conciliant légèreté des annotations et restrictions sur les alias. Nous définissons, dans un premier temps, un langage d'étude, qui s'inspire du langage C, et dans lequel le seul type de données mutable possible est le type des structures, auquel on accède uniquement à travers des pointeurs. Afin de structurer nos programmes, nous munissons notre langage d'une notion de module et des concepts issus de la théorie du raffinement tels que les variables abstraites que nous formalisons par des champs modèle, et les invariants de collage. Ceci nous permet d'écrire des programmes structurés en composants. L'introduction des invariants de données dans notre langage soulève des problématiques liées au partage de pointeurs. En effet, en cas d'alias, on risque de ne plus pouvoir garantir la validité de l'invariant de données d'une structure. Nous interdisons, alors l'aliasing (le partage de référence) dans notre langage. Pour contrôler les accès à la mémoire, nous définissons un système de type, basé sur la notion de régions. Cette contribution s'inspire de la théorie du raffinement et a pour but, de rendre les programmes les plus modulaires possible et leurs preuves les plus automatiques possible. Nous définissons, sur ce langage, un mécanisme de génération d'obligations de preuve en proposant un calcul de plus faible précondition incorporant du raffinement. Nous prouvons ensuite, la correction de ce mécanisme de génération d'obligations de preuve par une méthode originale, fondée sur la notion de sémantique bloquante, qui s'apparente à une preuve de type soundness et qui consiste donc, à prouver la préservation puis le progrès de ce calcul. Nous étendons, dans un deuxième temps, notre langage en levant partiellement la restriction liée au partage de références. Nous permettons, notamment, le partage de références lorsqu'aucun invariant de données n'est associé au type structure référencé. De plus, nous introduisons le type des tableaux, ainsi que les variables globales et l'affectation qui ne font pas partie du langage noyau. Pour chacune des extensions citées ci-dessus, nous étendons la définition et la preuve de correction du calcul de plus faible précondition en conséquence. Nous proposons enfin, une implantation de cette approche sous forme d'un greffon de Frama-C (http://frama-c.com/). Nous expérimentons notre implantation sur des exemples de modules implantant des structures de données complexes, en particulier des défis issus du challenge VACID0 (http://vacid. codeplex.com/), à savoir les tableaux creux (Sparse Array) et les tas binaires.

La vérification déductive de programmes consiste à annoter des programmes par une spécification, c'est-à-dire un ensemble de formules logiques décrivant le comportement du programme, et à prouver que les programmes vérifient bien leur spécification. Des outils tels que la plate-forme Why prennent en entrée un programme et sa spécification et calculent des formules logiques telles que, si elles sont prouvées, le programme vérifie sa spécification. Ces formules logiques peuvent être prouvées automatiquement ou à l'aide d'assistants de preuve.Lorsqu'un programme est écrit dans un langage supportant les alias de pointeurs, c'est-à-dire si plusieurs variables peuvent désigner la même case mémoire, alors le raisonnement sur le programme devient particulièrement ardu. Il est nécessaire de spécifier quels pointeurs peuvent être égaux ou non. Les invariants des structures de données, en particulier, sont plus difficiles à vérifier.Cette thèse propose un système de type permettant de structurer la mémoire de façon modulaire afin de contrôler les alias de pointeurs et les invariants de données. Il est basé sur les notions de région et de permission. Les programmes sont ensuite interprétés vers Why de telle façon que les pointeurs soient séparés au mieux, facilitant ainsi le raisonnement. Cette thèse propose aussi un mécanisme d'inférence permettant d'alléger le travail d'annotation des opérations de régions introduites par le langage. Un modèle est introduit pour décrire la sémantique du langage et prouver sa sûreté. En particulier, il est prouvé que si le type d'un pointeur affirme que celui-ci vérifie son invariant, alors cet invariant est effectivement vérifié dans le modèle. Cette thèse a fait l'objet d'une implémentation sous la forme d'un outil nommé Capucine. Plusieurs exemples ont été écrits pour illustrer le langage, et ont été vérifié à l'aide de Capucine. / Deductive verification consists in annotating programs by a specification, i.e. logic formulas which describe the behavior of the program, and prove that programs verify their specification. Tools such as the Why platform take a program and its specification as input and compute logic formulas such that, if they are valid, the program verifies its specification. These logic formulas can be proven automatically or using proof assistants.When a program is written in a language supporting pointer aliasing, i.e. if several variables may denote the same memory cell, then reasoning about the program becomes particularly tricky. It is necessary to specify which pointers may or may not be equal. Invariants of data structures, in particular, are harder to maintain.This thesis proposes a type system which allows to structure the heap in a modular fashion in order to control pointer aliases and data invariants. It is based on the notions of region and permission. Programs are then translated to Why such that pointers are separated as best as possible, to facilitate reasoning. This thesis also proposes an inference mechanism to alleviate the need to write region operations introduced by the language. A model is introduced to describe the semantics of the language and prove its safety. In particular, it is proven that if the type of a pointer tells that its invariant holds, then this invariant indeed holds in the model. This work has been implemented as a tool named Capucine. Several examples have been written to illustrate the language, and where verified using Capucine.

Le but de cette thèse est de spécifier et prouver des programmes avec pointeurs, tels que des programmes C, en utilisant des techniques de raffinement. L’approche proposée permet de faire un compromis entre les techniques complexes qui existent dans la littérature et ce qui est utilisable dans l’industrie, en conciliant légèreté des annotations et restrictions sur les alias. Nous définissons, dans un premier temps, un langage d’étude, qui s’inspire du langage C, et dans lequel le seul type de données mutable possible est le type des structures, auquel on accède uniquement à travers des pointeurs. Afin de structurer nos programmes, nous munissons notre langage d’une notion de module et des concepts issus de la théorie du raffinement tels que les variables abstraites que nous formalisons par des champs modèle, et les invariants de collage. Ceci nous permet d’écrire des programmes structurés en composants. L’introduction des invariants de données dans notre langage soulève des problématiques liées au partage de pointeurs. En effet, en cas d’alias, on risque de ne plus pouvoir garantir la validité de l’invariant de données d’une structure. Nous interdisons, alors l’aliasing (le partage de référence) dans notre langage. Pour contrôler les accès à la mémoire, nous définissons un système de type, basé sur la notion de régions. Cette contribution s’inspire de la théorie du raffinement et a pour but, de rendre les programmes les plus modulaires possible et leurs preuves les plus automatiques possible. Nous définissons, sur ce langage, un mécanisme de génération d’obligations de preuve en proposant un calcul de plus faible précondition incorporant du raffinement. Nous prouvons ensuite, la correction de ce mécanisme de génération d’obligations de preuve par une méthode originale, fondée sur la notion de sémantique bloquante, qui s’apparente à une preuve de type soundness et qui consiste donc, à prouver la préservation puis le progrès de ce calcul. Nous étendons, dans un deuxième temps, notre langage en levant partiellement la restriction liée au partage de références. Nous permettons, notamment, le partage de références lorsqu’aucun invariant de données n’est associé au type structure référencé. De plus, nous introduisons le type des tableaux, ainsi que les variables globales et l’affectation qui ne font pas partie du langage noyau. Pour chacune des extensions citées ci-dessus, nous étendons la définition et la preuve de correction du calcul de plus faible précondition en conséquence. Nous proposons enfin, une implantation de cette approche sous forme d’un greffon de Frama-C (http://frama-c.com/). Nous expérimentons notre implantation sur des exemples de modules implantant des structures de données complexes, en particulier des défis issus du challenge VACID0 (http://vacid. codeplex.com/), à savoir les tableaux creux (Sparse Array) et les tas binaires. / The purpose of this thesis is to specify and prove programs with pointers, such as C programs, using refinement techniques. The proposed approach allows a compromise between the complexe methods that exist in the literature and what is used in industry, reconciling lightness annotations and restrictions on the alias. We define, firstly, a language study, based on the C language, in which the only type of mutable data allowed is the type of structures, which can be accessed only through pointers. In order to structure our programs, we bring our language with a module notion and concepts issue from a refinement theory such as abstract variables that we formalize by model fields and gluing invariants. This allows us to write programs structured by components. Introducing invariants in our language raises issues related to aliasing. Indeed, in presence of alias, we might not be able to guarantee the validity of the invariant data structure. We forbid then the aliasing in our language. To control memory access, we define a type system based on the concept of regions. This contribution is based on the theory and refinement. It aims to make programs as modular as possible and proofs as automatic as possible. We define on this language, a mechanism for generation of proof obligations by proposing a weakest precondition calculus incorporating refinement. Next we prove the correction of this proof obligations generation mechnaism by an original method based on the concept of blocking semantic, which is similar to a proof of type soundness, and consists therefore, to proove the preservation and the progress of the defined calculus. Secondly, we extend our language by, partially, lifting the restrictions related to aliasing. We allow, in particular, sharing when no invariant is associated to the referenced data structure. In addition, we introduce the type of arrays, global variables, and assignment that are not part of the core language. For each of the extensions mentioned above, we extend the definition and correctness proof of the weakest precondition calculus accordingly. Finally, we propose an implementation of this approach as a Frama-C plugin(http ://frama-c.com/). We experimente our implantation on examples of modules implementing complex data structures, especially the challenges from the challenge VACID0 (http ://vacid. Codeplex.com /), namely sparse srrays and binary heaps.

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.