Résumé
Patrick Cousot, professeur à l’École Normale Supérieure, a présenté l’interprétation abstraite, qu’il développe avec son équipe depuis trente ans. L’idée est de faire calculer symboliquement le programme selon les mêmes lois d’exécution mais sur des données plus abstraites, comme des intervalles ou des polygones au lieu de nombres individuels. On peut alors approximer supérieurement l’ensemble des calculs possibles en temps fini, et détecter l’impossibilité de certaines erreurs critiques : accès à un tableau hors de ses bornes, division par zéro, débordement arithmétique (erreur qui a conduit à l’explosion d’Ariane 501).
L’interprétation abstraite repose sur un cadre général mathématiquement sophistiqué et sur le développement d’une collection de domaines abstraits (intervalles, octogones, ellipsoïdes, etc.). Son implémentation demande une ingénierie subtile pour bien combiner les propriétés des différents domaines. Elle a été industrialisée par plusieurs sociétés (Polyspace, AbsInt, etc.). L’équipe de P. Cousot a développé le logiciel Astrée, utilisé par Airbus pour vérifier l’absence d’exception arithmétique dans le code de pilotage de l’A380, ce qui constitue un des plus grands succès actuels de la vérification formelle.
