Dans la thèse nous présentons un cadre pour l'analyse statique de langages orientés objets qui tient compte des propriétés de modularité de ces langages. Il y a plusieurs défis à relever pour obtenir une analyse statique efficace de langages orientés objet. Tout d'abord, elle doit gérer les particularités de ces langages telles que l'héritage, le polymorphisme et la résolution de méthodes virtuelles. Deuxièmement, elle doit être modulaire. En fait, les programmes orientés objet typiques sont fait de plusieurs milliers de classes et une analyse monolithique du programmes complet peut être trop coûteuse pour être pratiquée. Troisièmement, la technologie orientée objet favorise la programmation par composants, en cela qu'un composant (une classe) est développée une fois pour toute et utilisée dans de nombreux contextes différents. Aussi, une analyse statique efficace doit pouvoir inférée des propriétés des composants valides pour toutes les instantiations possibles de contextes. Dans cette thèse, nous présentons une analyse qui relève les défis esquissés ci-dessus. En particulier, nous nous concentrons sur une analyse qui peut inférer des invariants de classe. Un invariant de classe est une propriété d'une classe valide pour chaque instanciation, avant et après l'exécution de n'importe quelle méthode de la classe. Notre analyse a plusieurs avantages. Elle est indépendante du langage, elle exploite la structure modulaire des langages orientés objet et elle gère les principales fonctionnalités de ces langages, à savoir l'héritage, le polymorphisme et l'encapsulation. Le cadre présenté dans cette thèse est très flexible. En particulier, il permet de régler finement l'analyse selon les trois axes orthogonaux suivants: - Domaine abstrait sous-jacent: une classe peut être analysée en utilisant soit un domaine abstrait générique soit un domaine abstrait symbolique de façon à obtenir une analyse plus efficace mais moins précise. - Gestion de l'héritage: une sous-classe peut être analysée soit directement, en expansant syntaxiquement la relation de sous-classe, soit indirectement, en utilisant l'invariant du parent afin d'éviter une explosion quadratique de la complexité. -Traitement des contextes d'instantiation: une classe peut être utilisée soit indépendamment du contexte, afin d'obtenir un résultat valable dans tous les contextes, soit en utilisant une approximation du contexte afin d'obtenir un résultat plus précis mais moins général.

Mes travaux de doctorat ont porté sur la certification de programmes impératifs utilisés dans des applications critiques. Les certificats établissent la validité des propriétés sémantiques des programmes et sont produits sous forme de preuves déductives vérifiables par machine. Le défi relevé dans cette thèse est d'automatiser la construction des preuves de correction de programmes. Nous avons suivie l'approche de Floyd-Hoare pour prouver que les propriétés sémantiques sont des invariants du programme et nous avons utilisé le le système Coq pour vérifier la validité des preuves. On considére ici le cas où les propriétés sémantiques sont calculées par des analyseurs statiques de programmes qui s'appuient sur la théorie de l'interprétation abstraite. Nous proposons une méthode d'instrumentation des analyseurs statiques de programmes afin de leur faire générer automatiquement un certificat pour chaque propriété sémantique calculée. L'instrumentation consiste à associer à certaines fonctions d'un analyseur statique des patrons de preuve qui à l'exécution généreront les certificats. De tels analyseurs instrumentés ne sont pas pour autant certifiés puisque leur correction pour toutes leurs entrées possibles n'est pas garantie, néanmoins ils sont capables de justifier par une preuve formelle la correction du résultat de chacun de leurs calculs. Bien sûr, si pour une entrée possible l'exécution de l'analyseur est boguée le résultat sera erroné et la justification produite ne sera pas une preuve valide; elle sera rejettée par le vérificateur de preuves. Cette approche permet de certifier avec un très haut-niveau de confiance (celui du vérificateur de preuves) les résultats d'outils existants, même à l'état de prototypes. Pour que l'instrumentation soit applicable en pratique, nous avons cherché à limiter le nombre de fonctions à instrumenter. Nous avons dégagé un ensemble restreint de fonctions, commun à tout analyseur, à instrumenter pour qu'un analyseur existant devienne un outil de certification automatique. Nous avons appliqué cette technique d'instrumentation à un analyseur de programmes manipulant des tableaux qui s'appuie sur des domaines abstraits non triviaux. Cet analyseur calcule des propriétés sur le contenu des tableaux manipulés par les programmes et, grâce à notre instrumentation, génère désormais des certificats vérifiables par Coq attestant de la validité des propriétés découvertes par l'analyse statique. Nous montrons enfin comment utiliser cet analyseur instrumenté pour certifier un protocole de communication pour systèmes multi-tâches destiné à l'avionique. La garantie de la correction des programmes est cruciale dans le domaine des systèmes embarqués. Face aux coûts et la durée d'une procédure de certification formelle, le développement d'outils automatiques de certification représente un enjeu économique majeur. La transformation, par instrumentation, d'outils d'analyses existants en outils de certification est une réponse possible qui évite la certification des outils d'analyse.