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.
| Identifer | oai:union.ndltd.org:CCSD/oai:tel.archives-ouvertes.fr:tel-00136630 |
| Date | 06 December 2004 |
| Creators | Miné, Antoine |
| Publisher | Ecole Polytechnique X |
| Source Sets | CCSD theses-EN-ligne, France |
| Language | English |
| Detected Language | French |
| Type | PhD thesis |
Page generated in 0.0023 seconds