Abstract FR:

L'analyse statique désigne des méthodes automatiques pour extraire des propriétés des programmes. Malheureusement, les ordinateurs n'ont souvent pas les ressources suffisantes pour analyser de gros programmes. Pour remédier à ce problème, nous proposons une méthodologie d'analyse modulaire qui calque la structure de l'analyse sur la structure de modules des programmes. Dans ce cadre, chaque fragment de programme est analysé séparément. De fait, le coût d'analyse est factorisé et une part de l'analyse globale est calculée à l'avance. Dans cette thèse, nous avons défini ce qu'était une méthode de résolution modulaire et identifié la notion de résolution modulaire optimale. Nous avons appliqué ces principes théoriques à une analyse de flot de contrôle et à une analyse de sécurité. Dans ces deux cas, nous avons proposé des approximations et/ou des restrictions pour assurer la terminaison de la résolution modulaire optimale. Notre conviction est que toute analyse s'adapte à notre cadre.