Cousot

Elle grandit dans une société en pleine mutation, marquée par les transformations postcoloniales et les ambitions modernisatrices du jeune État tunisien. Très tôt, elle développe un goût prononcé pour les mathématiques et la logique, disciplines dans lesquelles elle se distingue dès le lycée. Elle poursuit des études supérieures brillantes, d'abord en Tunisie, puis en France, où elle s'installe pour mener une carrière scientifique de haut niveau dans le domaine de l'informatique théorique.

Elle s'oriente vers l'analyse statique des programmes, une branche de l'informatique consacrée à la vérification formelle de la correction des logiciels. Aux côtés de son mari, Patrick Cousot (ci-dessous), elle cofonde à la fin des années 1970 le concept fondamental d'interprétation abstraite , une méthode mathématique rigoureuse permettant de prédire le comportement des programmes informatiques sans les exécuter. Cette approche repose sur des fondements logiques et algébriques très solides et ouvre la voie à des applications en sécurité informatique, en analyse de performances, et en fiabilité des logiciels critiques.

Le couple Cousot publie des travaux pionniers qui auront un impact international considérable, notamment l'article fondateur de 1977 qui structure formellement le cadre théorique de l'interprétation abstraite. Radhia Cousot participe activement au développement de cette théorie, à son élargissement vers de nouveaux langages de programmation, et à sa mise en œuvre dans des outils concrets, comme Astrée, utilisé notamment dans l'aéronautique pour garantir l'absence d'erreurs d'exécution dans les systèmes embarqués.

À partir de cette époque, il travaille intensément sur les fondements mathématiques permettant de raisonner de manière formelle sur les comportements d'un programme informatique sans l'exécuter. Avec son épouse et collaboratrice Radhia Cousot, il publie en 1977 l'article fondateur de l'interprétation abstraite, qui devient une référence incontournable. Ce cadre théorique permet de détecter automatiquement des erreurs, des fuites de mémoire ou des violations de sécurité dans des programmes, avec des garanties formelles de correction. L'approche est adoptée dans l'industrie, notamment chez Airbus, Astrium ou Dassault Aviation, et inspire de nombreux outils, dont Astrée, un analyseur statique pour le code embarqué critique, codé en C.

Professeur au sein de plusieurs institutions prestigieuses, il enseigne à l'École normale supérieure de Paris et à l'Université de New York (NYU) où il rejoint le Courant Institute of Mathematical Sciences. Il influence une génération entière de chercheurs en informatique, tout en continuant de publier des travaux fondamentaux, souvent au croisement entre logique mathématique, théorie des domaines et vérification formelle.

Toujours actif dans la recherche, Patrick Cousot poursuit son objectif d'offrir des garanties solides et mathématiquement fondées sur le bon fonctionnement des systèmes logiciels critiques