Dr. Radhia Cousot

A French computer scientist who, together with her husband Patrick, is the originator of Abstract Interpretation, an influential technique in formal methods 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; and 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). Born in Sakiet Sidi Youssef in Tunisia, 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, France in 1985 under the supervision of Claude Pair (fr). In her thesis, she advanced the semantics, proof, and static analysis methods for concurrent and parallel programs. She 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 in Paris, France from 2006 to 2014. She was at the origin of the contacts in January 1999 with Airbus (an aircraft manufacturing division of Airbus Group based in Blagnac, France), which led to the development of Astr?e run-time error analyzer from 2001 on. Astr?e is a tool for sound static program analysis of embedded control/command software developed at the ?cole Normale Sup?rieure and now distributed by AbsInt GmbH, a German software company specialized on static analysis. Astr?e is used in transportation, space, and medical software industry. The Astr?e system for the analysis of real-time embedded systems, built under her and her husband?s supervision, was a watershed in the history of program analysis. In 2003, Astr?e was used to prove, completely automatically, that the primary flight control software of the Airbus A340 fly-by-wire system was free of runtime errors like division by zero, array bound violation, or violation of user-written assertions. In 2008, Astr?e was able to automatically prove that the automated docking software of the Jules Verne automated transfer vehicle, used to transfer payloads to the International Space Station, was free of runtime errors. Along with Patrick, she received the ACM SIGPLAN in 2013 and the IEEE Computer Society IEEE Computer Society Harlan D. Mills award in 2014 for ?For the invention of ?abstract interpretation?, development of tool support, and its practical application?. Since September 2014, the Radhia Cousot best young researcher paper award is attributed annually by the program chair on behalf of the program committee of the Static Analysis Symposia (SAS). One recipient is in 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. She passed away in the summer of 2014 after a long struggle with cancer.