Accueil du site > Vie de la recherche > Actualités institutionnelles




Recherchez sur ce site


Disparition de Radhia Cousot

C’est avec une grande tristesse que l’Institut des sciences de l’information et de leurs interactions a appris le décès de Radhia Cousot, survenu le 1er mai 2014, à l’âge de 66 ans.

Après un doctorat en mathématiques, Radhia Cousot a rejoint le CNRS en 1980. Elle a travaillé au sein de l’Université Henri Poincaré de Nancy (1980-1983), de l’Université Paris-Sud à Orsay (1984-1988), puis de l’École polytechnique (1989-2008). Elle y a dirigé, à partir de 1991 l’équipe de recherche « Sémantique, preuve et interprétation abstraite ». Elle a rejoint en 2006 l’École Normale Supérieure.

Radhia Cousot a inventé, avec Patrick Cousot, la théorie de l’interprétation abstraite. C’est une théorie fondamentale qui permet de donner un cadre unifié et formel à l’ensemble des méthodes liées à la vérification des systèmes informatiques (et biologiques) ; il s’agit d’abord de la sémantique et la spécification formelles (qui décrivent les comportements des systèmes), de l’analyse statique, essentielle pour la vérification (qui permet de déduire automatiquement les propriétés des systèmes à partir de leurs descriptions formelles), de la preuve (qui vérifie — à la main, avec un démonstrateur ou un assistant de preuve— que les systèmes ont bien les propriétés attendues), et enfin de la vérification proprement dite (qui permet de vérifier de manière automatique que les systèmes ont les propriétés attendues).

Dans leur travail original, Radhia et Patrick Cousot ont d’abord montré comment on pouvait relier une analyse statique à la sémantique standard d’un langage. Ils ont ainsi, et pour la première fois, donné une définition formelle de l’analyse statique et décrit une méthodologie claire qui permet de la concevoir et de prouver son exactitude. Ils ont fourni les éléments essentielsde l’interprétation abstraite, encore en usage aujourd’hui ; citons l’itération chaotique, les méthodes d’extrapolation par élargissement-rétrécissement , les combinaisons d’abstractions, et de nombreux domaines abstraits. Cet ensemble remarquable de méthodes formelles a pu ensuite se concrétiser sous forme de bibliothèques largement utilisées.

Enfin, Radhia et Patrick Cousot, avec leurs équipes, ont contribué à diffuser l’analyse statique dans le monde socio-économique, en démontrant son utilité et son efficacité. Ils ont développé l’analyseur statique Astrée (Analyseur statique de logiciels temps-réel embarqués), qui permet de vérifier à l’avance la correction du code présent dans les systèmes embarqués. Ce logiciel a d’abord permis la « sécurisation » des logiciels de vol de l’Airbus 380 ; il est également utilisé dans l’industrie médicale, automobile et aérospatiale. C’est l’un des plus grands succès de la vérification de programme à ce jour.

En 2013, Radhia Cousot a reçu, en commun avec Patrick Cousot, l’ACM SIGPLAN Programming Languages Achievement Award. Le mois dernier, ils ont reçu une autre récompense prestigieuse, le 2014 Harlan D. Mills Award de l’IEEE Computer Society, qui distingue les contributions des sciences de l’information, à la fois théoriques et applicatives, en récompensant tout particulièrement les travaux théoriques qui mènent à des logiciels vraiment utilisés.

Sur un plan plus personnel, Radhia Cousot était connue pour sa gentillesse, notamment envers les doctorants et autres jeunes chercheurs.