Jump to content

Radhia Cousot

From Wikipedia, the free encyclopedia

This is an old revision of this page, as edited by AnomieBOT (talk | contribs) at 03:39, 16 November 2016 (Substing templates: {{ill}}. See User:AnomieBOT/docs/TemplateSubster for info.). The present address (URL) is a permanent link to this revision, which may differ significantly from the current revision.

Radhia Cousot
Born(1947-08-06)6 August 1947
Sakiet Sidi Youssef, Tunisia
Died1 May 2014(2014-05-01) (aged 67)
New York City
NationalityFrench
Alma materInstitut National Polytechnique de Lorraine
Known forAbstract interpretation
AwardsACM SIGPLAN Programming Languages Achievement Award
IEEE Computer Society Harlan D. Mills Award
Scientific career
FieldsComputer science
Thesis Fondements des méthodes de preuve d'invariance et de fatalité de programmes parallèles  (1985)
Doctoral advisorClaude Pair

Radhia Cousot (6 August 1947 – 1 May 2014)[1] was a French computer scientist known for inventing Abstract interpretation.

Studies

Radhia Cousot was born on 6 August 1947, in Sakiet Sidi Youssef in Tunisia, where she survived the massacre of the children in her school on February 8, 1958. She then went to the Lycée de jeunes filles at Sousse, the Lycée français at Algiers and then the Polytechnic School of Algiers (where she was ranked 1st and the only woman). She specialized in mathematical optimization and integer linear programming. Supported by a UNESCO fellowship (1972–1975), she obtained a master's degree in Computer Science (Diplôme d'études approfondies (DEA)) at the Joseph Fourier University of Grenoble in 1972. She obtained her Doctorate ès Sciences/State Doctorate in Mathematics in Nancy in 1985 under the supervision of Claude Pair [fr].[nb 1]

Career

Radhia Cousot was appointed Associate research scientist at the IMAG laboratory of the Joseph Fourier University of Grenoble (1975–1979) and, from 1980 on, at the Centre national de la recherche scientifique, as junior research scientist, research scientist, senior research scientist, and senior research scientist emerita at the Computer Science laboratories of the Henri Poincaré University of Nancy (1980–1983), the University of Paris-Sud at Orsay (1984–1988), the École Polytechnique (1989–2008) where from 1991 she headed the research team “Semantics, Proof and Abstract interpretation”, and the École Normale Supérieure (2006–2014).

Scientific achievements

Together with her husband Patrick, Radhia Cousot is the originator of abstract interpretation,[2][3] an influential technique in formal methods. Abstract interpretation is based on three main ideas.

  1. Any reasoning/proof/static analysis on a computer system refers to a semantics describing, at some level of abstraction, its possible executions.
  2. The reasoning/proof/static analysis should abstract away all semantic properties irrelevant to the reasoning.
  3. Because of undecidability, sound, fully automated, and always terminating reasonings on/proofs/static analysis of computer systems must perform mathematical inductions in the abstract and so, can only be approximate (even with finiteness and decidability hypothesis, because of combinatorial explosion beyond tiny systems).

In her thesis, Radhia Cousot advanced the semantics, proof, and static analysis methods for concurrent and parallel programs.[4]

Radhia Cousot is at the origin of the contacts with Airbus in January 1999 that lead to the development of Astrée run-time error analyzer from 2001 on, a tool for sound static program analysis of embedded control/command software developed at the École Normale Supérieure[5] and now distributed by AbsInt GmbH,[6] a German software company specialized on static analysis. Astrée is used in transportation, space, and medical software industry.

Awards

With Patrick Cousot, she received the ACM SIGPLAN [7] in 2013 and the IEEE Computer Society IEEE Computer Society Harlan D. Mills award [8] in 2014 for “ For the invention of ‘abstract interpretation’, development of tool support, and its practical application ”.

Radhia Cousot best young researcher paper award

Since September 2014, the Radhia Cousot best young researcher paper award[9] is attributed annually by the program chair on behalf of the program committee of the Static Analysis Symposia (SAS).[10]

  • 2014 (Munich, Germany): Aleksandar Chakarov (University of Colorado, Boulder, CO, USA), Expectation invariants for probabilistic program loops as fixed points (with Sriram Sankaranarayanan), M. Müller-Olm & H. Seidl (Eds.): SAS 2014, LNCS 8723, pp. 85–100, Springer

Notes

  1. ^ In the 1980s, there existed in France two levels of PhDs, the higher one, the Doctorate ès Sciences/State Doctorate being necessary to access professorships. It has since been replaced by the habilitation.

References

  1. ^ [1]
  2. ^ Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, POPL '77 Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, Pages 238-252, ACM New York, NY, USA
  3. ^ Systematic design of program analysis frameworks, POPL '79 Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, Pages 269-282, ACM New York, NY, USA
  4. ^ Fondements des méthodes de preuve d'invariance et de fatalité de programmes parallèles. Radhia Cousot. Thèse ès Sciences Mathématiques, Institut national polytechnique de Lorraine, Nancy, France, 15 November 1985. France
  5. ^ Home page of the Astrée Static Analyzer at ENS
  6. ^ Home page of the Astrée Static Analyzer at AbsInt
  7. ^ ACM SIGPLAN Programming Languages Achievement Award
  8. ^ IEEE Computer Society Harlan D. Mills
  9. ^ Radhia Cousot best young researcher paper award
  10. ^ Static Analysis Symposia (SAS)
Retrieved from "https://en.wikipedia.org/w/index.php?title=Radhia_Cousot&oldid=749778552"