Cette thèse s'inscrit dans la démarche de preuve de programmes à l'aide de vérification déductive. La vérification déductive consiste à produire, à partir des sources d'un programme, c'est-à-dire ce qu'il fait, et de sa spécification, c'est-à-dire ce qu'il est sensé faire, une conjecture qui si elle est vraie alors le programme et sa spécification concordent. On utilise principalement des démonstrateurs automatiques pour montrer la validité de ces formules. Quand ons'intéresse à la preuve de programmes qui utilisent des structures de données allouées en mémoire, il est élégant et efficace de spécifier son programme en utilisant la logique de séparation qui est apparu il y a une dizaine d'année. Cela implique de prouver des conjectures comportant les connectives de la logique de séparation, or les démonstrateurs automatiques ont surtout fait des progrès dans la logique du premier ordre qui ne les contient pas.Ce travail de thèse propose des techniques pour que les idées de la logique de séparation puissent apparaître dans les spécifications tout en conservant la possibilité d'utiliser des démonstrateurs pour la logique du premier ordre. Cependant les conjectures que l'ont produit ne sont pas dans la même logique du premier ordre que celles des démonstrateurs. Pour permettre une plus grande automatisation, ce travail de thèse a également défini de nouvelles conversions entre la logique polymorphe du premier ordre et la logique multi-sortée dupremier ordre utilisé par la plupart des démonstrateurs.La première partie a donné lieu à une implémentation dans l'outil Jessie, la seconde a donné lieu à une participation conséquente à l'écriture de l'outil Why3 et particulièrement dans l'architecture et écriture des transformations qui implémentent ces simplifications et conversions. / This thesis comes within the domain of proofs of programs by deductive verification. The deductive verification generates from a program source and its specification a mathematical formula whose validity proves that the program follows its specification. The program source describes what the program does and its specification represents what the program should do. The validity of the formula is mainly verified by automatic provers. During the last ten years separation logic has shown to be an elegant way to deal with programs which use data-structures with pointers. However it requires a specific logical language, provers, and specific reasoning techniques.This thesis introduces a technique to express ideas from separation logic in the traditional framework of deductive verification. Unfortunately the mathematical formulas produced are not in the same first-order logic than the ones of provers. Thus this work defines new conversions between the polymorphic first-order logic and the many-sorted logic used by most proves.The first part of this thesis leads to an implementation in the Jessietool. The second part results in an important participation to the writing of the Why3 tool, in particular in the architecture and writing of the transformations which implement these conversions.

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.