Détails sur le séminaire

Résumé : Les travaux menés dans cette thèse portent 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. Ils 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 système Coq pour vérifier la validité des preuves.
Dans nos travaux, on considére 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 et s\'appuyant 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 il 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.



Jury composé de:
Laurence Pierre (Professeur UJF), Présidente proposée
Thomas Jensen (DR IRISA), Rapporteur
Olga Kouchnarenko (Professeur Univ de Franche-Comté), Rapporteur
Solange Coupet-Grimal (Univ de Provence), Examinateur
Gilles Barthe (Professeur IMDEA Software Faculty), Examinateur
Michaël Périn (MCF UJF), Directeur de thèse