# Radhia Cousot

Radhia Cousot (Sakiet Sidi Youssef, Tunísia, 6 d'agost de 1947 - Nova York, 1 de maig de 2014) va ser una científica, matemàtica i informàtica francesa coneguda per inventar la interpretació abstracta –una teoria d'aproximació de la semàntica dels programes informàtics, que ofereix un marc unificat als diversos mètodes vinculats a la verificació de sistemes informàtics i biològics.

## Estudis

Radhia Cousot va néixer el 6 d'agost de 1947 a Sakiet Sidi Youssef, a Tunísia, on va sobreviure a la massacre dels nens de la seva escola el 8 de febrer de 1958. Després va anar al Lycée de jeunes filles de Sousse, al Lycée français d'Alger i després a l'Escola Politècnica d'Alger (on va ser la primera i única dona). Es va especialitzar en optimització matemàtica i programació lineal. Amb el suport d'una beca de la UNESCO (1972–1975), va obtenir un màster en Informàtica (DEA) a la Universitat Joseph Fourier de Grenoble el 1972. Va obtenir el doctorat en ciències / doctorat estatal en matemàtiques a Nancy el 1985.

## Carrera

Radhia Cousot va ser nomenada investigadora associada al laboratori IMAG de la Universitat Joseph Fourier de Grenoble (1975–1979) i, a partir de 1980, al Centre national de la recherche scientifique, com a investigadora junior, científica investigadora, científica investigadora sènior, i investigadora sènior emèrita als laboratoris d'informàtica de la Universitat Henri Poincaré de Nancy (1980–1983), la Universitat de Paris-Sud a Orsay (1984–1988), l'École Polytechnique (1989–2008), on des de 1991 va dirigir l'equip de recerca "Semàntica, prova i interpretació abstracta" i l'École Normale Supérieure (2006–2014).

## Assoliments científics

Juntament amb el seu marit Patrick, Radhia Cousot és la creadora de la interpretació abstracta, una tècnica influent en els mètodes formals. La interpretació abstracta es basa en tres idees principals.
* Qualsevol raonament/prova/anàlisi estàtica en un sistema informàtic fa referència a una semàntica que descriu, en algun nivell d'abstracció, les seves possibles execucions.
* El raonament/prova/anàlisi estàtica hauria d'abstraure totes les propietats semàntiques irrellevants per al raonament.
* A causa de la indecidibilitat, els raonaments sòlids, totalment automatitzats i sempre acabant sobre proves/anàlisi estàtica dels sistemes informàtics han de realitzar inducció matemàtica en abstracte i, per tant, només poden ser aproximades (fins i tot amb la hipòtesi de la finitud i la decidibilitat, a causa de l'explosió combinatòria més enllà de sistemes minúsculs).
En la seva tesi, Radhia Cousot va avançar la semàntica, la demostració i els mètodes d'anàlisi estàtica per a programes concurrents i paral·lels.
Radhia Cousot és l'origen dels contactes amb Airbus el gener de 1999 que van portar al desenvolupament de l'analitzador d'errors de temps d'execució Astrée a partir de 2001, una eina per a l'anàlisi de programes estàtics sonors del programari de control/comandament incrustat desenvolupat a l'École Normale Supérieure i ara distribuït per AbsInt GmbH, una empresa de programari alemanya especialitzada en anàlisi estàtica. Astrée s'utilitza en les indústries del transport, l'espai i el programari mèdic.

## Premis

Amb Patrick Cousot, va rebre l'ACM SIGPLAN Programming Languages Achievement Award el 2013 i l'IEEE Computer Society Harlan D. Mills award el 2014 per "la invenció de la 'interpretació abstracta', el desenvolupament del suport d'eines i la seva aplicació pràctica".

## Premi Radhia Cousot al millor treball investigador jove

Des del setembre de 2014, el president del programa atorga anualment el premi Radhia Cousot al millor treball investigador jove en nom del comitè del programa del Simposi d'anàlisi estàtica (SAS).

## Referències

* ↑ Macho Stadler, Marta. «Radhia Cousot, especialista en ciencias de la computación» (en castellà), 06-08-2015. [Consulta: 14 març 2024].
* 1 2 Chaudhuri, Swarat. «Radhia Cousot» (en anglès). The PL Enthusiast, 09-06-2014. [Consulta: 14 març 2024].
* ↑ Cousot, Patrick. «Abstract interpretation». A: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. ACM, 1 January 1977, p. 238–252. DOI 10.1145/512950.512973.
* ↑ Cousot, Patrick. «Systematic design of program analysis frameworks». A: Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages - POPL '79. ACM, 1 January 1979, p. 269–282. DOI 10.1145/567752.567778.
* ↑ Cousot, Radhia; Cousot, Patrick. «Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints» (en anglès). [Consulta: març 2024].
* ↑ «R. Cousot, Fondements des méthodes de preuve d'invariance et de fatalité de programmes parallèles.». www.di.ens.fr. Arxivat de l'original el 2015-09-23. [Consulta: 14 març 2024].
* ↑ «Astrée Runtime Error Analyzer». www.absint.com.
* ↑ «The Astrée Static Analyzer». [Consulta: 14 març 2024].
* ↑ «Programming Languages Achievement Award». www.sigplan.org.
* ↑ «Harlan D. Mills Award • IEEE Computer Society». www.computer.org.
* ↑ «Static Analysis Symposia Central Site». staticanalysis.org.