Un exposé sur l'Interprétation abstraite

À Paris 6, le jeudi 29 septembre

L'auteur de ce sujet a trouvé une solution à son problème.
Auteur du sujet

Cliquez pour voir l'affiche en grand

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 !


  1. 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

+3 -0
Auteur du sujet

C'est accessible (au sens où on peut comprendre l'idée générale) à quel niveau tu dirais ? Le sujet m'intéresse mais je connais ni l'une ni l'autre des notions que tu indiques en note, vu que je sors de taupe.

+0 -0

J'y serai certainement aussi.

C'est accessible (au sens où on peut comprendre l'idée générale) à quel niveau tu dirais ? Le sujet m'intéresse mais je connais ni l'une ni l'autre des notions que tu indiques en note, vu que je sors de taupe.

Viens ! Les colloquiums de P6 sont ouverts à tous, donc c'est censé a priori être accessible. Après, ça dépend bien sûr des orateurs et des sujets, mais si ça t'intéresse, n'hésite pas. Les notions citées par Lz36GQfANCkOchnWu2yv ne sont en tout cas certainement pas des prérequis pour comprendre la présentation, mais plutôt pour établir le cadre formel de l'interprétation abstraite (c'est un exposé de présentation, pas un cours magistral sur le sujet).

Et puis, au pire, si tu comprends pas, on pourra en parler après !

Édité par Eusèbe

+1 -0
Auteur du sujet

C'est accessible (au sens où on peut comprendre l'idée générale) à quel niveau tu dirais ? Le sujet m'intéresse mais je connais ni l'une ni l'autre des notions que tu indiques en note, vu que je sors de taupe.

Grimur

Le plus difficile ça sera certainement de supporter l'accent de l'orateur.

+0 -0
Auteur du sujet

Salut,

À cause de la venue de François Hollande sur le campus Jussieu, l'entrée risque d'être interdite au public entre 13h30 et 16h30 si tout se passe bien. Ne venez pas trop tôt pour le cocktail.

Edit : peut-être que c'est seulement pour les véhicules en fait.

Édité par anonyme

+0 -0
Auteur du sujet

J'ai plus ou moins rien entendu de ce qu'il disait quand c'était en anglais (et c'est pas faute de bien comprendre et parler l'anglais), mais les slides plus la page Wiki ont suffi. J'ai compris l'idée générale mais pour ce qui est de la mise en pratique c'est autre chose, vu que je n'ai pas compris les formalismes qu'il a introduit vers la fin (à part le coup du point fixe).

C'était intéressant comme prévu, mais comme prévu aussi j'ai rien entendu.

Édité par anonyme

+0 -0
Vous devez être connecté pour pouvoir poster un message.
Connexion

Pas encore inscrit ?

Créez un compte en une minute pour profiter pleinement de toutes les fonctionnalités de Zeste de Savoir. Ici, tout est gratuit et sans publicité.
Créer un compte