Bonjour à tous,
Ce jeudi 29 septembre, à Jussieu (Paris 6), aura lieu un exposé de Patrick Cousot sur l'interprétation abstraite.
Pour faire court, l'interprétation abstraite est un cadre à la fois théorique et pratique qu'il a proposé à la fin des années 70 pour faire de l'analyse statique, c'est-à-dire prouver des propriétés sur les programmes sans avoir à les exécuter.
C'est une méthode qui a porté ses fruits : elle est utilisée notamment à leur échelle par Facebook et Google, et l'analyseur Astrée a permis de prouver l'absence d'erreurs à l'exécution dans les programmes de commande de vol de deux avions Airbus, l'A340 et l'A380.
Le problème principal qui s'est posé pour écrire de telles analyses est celui de l'indécidabilité : dans le cas général, il est impossible d'écrire un programme qui termine à coup sûr et qui calcule tous les comportements possibles d'un autre programme. Le framework de l'interprétation abstraite permet d'écrire des analyses sûres, c'est-à-dire qui n'oublient aucun comportement possible du programme (mais qui peuvent éventuellement en rajouter, introduisant des imprécisions). Ainsi, quand un programme est déclaré absent d'une certaine classe de bugs, on est certain qu'il est impossible que ces bugs apparaissent (à moins que l'analyseur soit lui-même buggé, mais c'est une autre histoire, et on sait écrire des analyseurs en lesquels on puisse raisonnablement avoir confiance).
L'interprétation abstraite et, plus généralement, de nombreux pans de l'analyse statique sont des sujets qui appartiennent au vaste domaine des méthodes formelles, qui consistent à utiliser des outils mathématiques éprouvés pour obtenir une confiance très forte dans les programmes qu'on écrit.
Il risque donc d'y avoir pas mal de formules mathématiques1, mais n'hésitez pas à venir quand même : derrière la formalisation qui peut sembler certes un peu aride au premier abord, il y a de nombreuses intuitions de programmeur derrière ce framework, qui, en plus d'être souvent assez amusantes, apportent un regard nouveau qui ne peut qu'être bénéfique sur la programmation.
Voilà, c'est à 18h à Jussieu ce jeudi, et j'y serai. Ce sera en anglais, mais dans un anglais technique avec un accent français, donc relativement accessible. Il y a même un cocktail avant pour ceux qui assisteront à la présentation (on peut y aller ensemble si vous êtes timide), alors n'hésitez pas !
-
Pour les plus curieux, l'interprétation abstraite est fondée sur un outil mathématique appelé correspondance de Galois, et on y travaille beaucoup avec des structures de treillis. ↩
