Le sujet de cette thèse est le développement de méthodes pour l'analyse automatique des programmes informatiques. Une des applications majeures est la conception d'outils pour découvrir les erreurs de programmations avant qu'elles ne se produisent, ce qui est crucial à l'heure où des tâches critiques mais complexes sont confiées à des ordinateurs. Nous nous plaçons dans le cadre de l'interprétation abstraite, qui est une théorie de l'approximation sûre des sémantiques de programmes, et nous nous intéressons en particulier aux domaines abstraits numériques spécialisés dans la découverte automatique des propriétés des variables numérique d'un programme.<br />Dans cette thèse, nous introduisons plusieurs nouveaux domaines numériques abstraits et en particulier le domaine des zones (permettant de découvrir des invariants de la forme X-Y≤c, des zones de congruence (X≡Y+c [b]) et des octogones (±X ±Y≤c). Ces domaines sont basés sur les concepts existants de graphe de potentiel, de matrice de différences bornées et sur l'algorithmique des plus courts chemins. Ils sont intermédiaires, en terme de précision et de coût, entre les domaines non relationnels (tel celui des intervalles), très peu précis, et les domaines relationnels classiques (tel celui des polyèdres), très coûteux. Nous les nommons " faiblement relationnels ". Nous présentons également des méthodes permettant d'appliquer les domaines relationnels à l'analyse de nombres à virgule flottante, jusqu'à présent uniquement réalisable par des domaines non relationnels donc peu précis. Enfin, nous présentons des méthodes génériques dites de " linéarisation " et de " propagation de constantes symboliques " permettant d'améliorer la précision de tout domaine numérique, pour un surcoût réduit.<br />Les méthodes introduites dans cette thèse ont été intégrées à Astrée, un analyseur spécialisé dans la vérification de logiciels embarqués critiques et se sont révélées indispensables pour prouver l'absence d'erreurs à l'exécution de logiciels de commande de vol électrique. Ces résultats expérimentaux viennent justifier l'intérêt de nos méthodes pour des cadre d'applications réelles.

Le sujet de cette thèse est le développement de méthodes pour la découverte automatique des propriétés des variables numériques d'un programme. Nous nous plaçons dans le cadre de l'interprétation abstraite et introduisons plusieurs nouveaux domaines numériques, dont celui des octogones, de coût et de précision intermédiaires entre les domaines non relationnels (peu précis) et relationnels (coûteux) existants. Nous présentons leur adaptation à l'analyse des nombres à virgule flottante, jusqu'à présent limitée aux domaines non relationnels. Enfin, nous présentons les méthodes génériques de linéarisation et de propagation symbolique améliorant leur précision pour un surcoût réduit. Les méthodes introduites dans cette thèse ont été intégr! ées à l'analyseur Astrée et appliquées à la preuve d'absence d'erreurs dans le logiciel embarqué critique de commande de vol des avions Airbus A340, justifiant ainsi l'intérêt de nos méthodes pour des cadres d'applications réelles.