Radhia Cousot - Radhia Cousot

Radhia Cousot
RadhiaCousot - Picture.jpg
narozený ( 08.06.1947 ) 6. srpna 1947
Sakiet Sidi Youssef , Tunisko
Zemřel 1. května 2014 (01.05.2014) (ve věku 67)
New York City
Národnost francouzština
Alma mater Institut National Polytechnique de Lorraine
Známý jako Abstraktní interpretace
Manžel (y) Patrick Cousot
Ocenění ACM SIGPLAN Programming Languages ​​Achievement Award Cena
IEEE Computer Society Harlan D. Mills
Vědecká kariéra
Pole Počítačová věda
Teze Fondements des méthodes de preuve d'invariance et de fatalité de programs parallèles   (1985)
Doktorský poradce Claude Pair

Radhia Cousot (6. srpna 1947 - 1. května 2014) byla francouzská počítačová vědkyně známá vymýšlením abstraktní interpretace .

Studie

Radhia Cousot se narodila 6. srpna 1947 v Sakiet Sidi Youssef v Tunisku , kde 8. února 1958 přežila masakr dětí ve své škole . Poté šla na Lycée de jeunes filles v Sousse , Lycée français v Alžíru a poté na Polytechnickou školu v Alžíru (kde se umístila na 1. a jediné ženě). Specializovala se na matematickou optimalizaci a celočíselné lineární programování . S podporou stipendia UNESCO (1972–1975) získala v roce 1972. magisterský titul v oboru výpočetní techniky ( Diplôme d'études accfondies (DEA) ) na univerzitě Josepha Fouriera v Grenoblu. Získala doktorát věd / státní doktorát z matematiky. v Nancy v roce 1985 pod dohledem Clauda Pair  [ fr ] .

Kariéra

Radhia Cousotová byla jmenována přidruženou vědeckou pracovnicí v laboratoři IMAG na Univerzitě Josepha Fouriera v Grenoblu (1975–1979) a od roku 1980 v Centre national de la recherche scientifique , jako vědecký pracovník, vědecký pracovník, vedoucí vědecký pracovník, a vedoucí vědecký pracovník emerita v počítačových vědních laboratořích Henri Poincaré University v Nancy (1980–1983), University of Paris-Sud v Orsay (1984–1988), École Polytechnique (1989–2008), kde od roku 1991 vedla výzkumný tým „Sémantika, důkaz a abstraktní interpretace“ a École Normale Supérieure (2006–2014).

Vědecké úspěchy

Spolu s manželem Patrickem je Radhia Cousot původcem abstraktní interpretace , vlivné techniky formálních metod . Abstraktní interpretace je založena na třech hlavních myšlenkách.

  1. Jakákoli úvaha / důkaz / statická analýza v počítačovém systému odkazuje na sémantiku popisující na určité úrovni abstrakce její možné provedení.
  2. Argumentace / důkaz / statická analýza by měla abstrahovat všechny sémantické vlastnosti irelevantní pro uvažování.
  3. Kvůli nerozhodnutelnosti musí spolehlivé, plně automatizované a vždy končící úvahy v / proofs / statické analýze počítačových systémů provádět matematické indukce abstraktně, a proto mohou být pouze přibližné (dokonce s hypotézou konečnosti a rozhodovatelnosti, kvůli kombinatorické explozi přesahující malé systémy).

Ve své diplomové práci Radhia Cousot rozšířila metody sémantiky, proof a statické analýzy pro souběžné a paralelní programy.

Radhia Cousot je na počátku kontaktů s Airbusem v lednu 1999, které vedly k vývoji Astrée chyby analyzátoru běhu od roku nástroje pro zvuk 2001 analýzu statické údaje o vložené control / příkazového softwaru vyvinutého na École Normale Supérieure a nyní distribuuje německá softwarová společnost AbsInt GmbH specializující se na statickou analýzu. Astrée se používá v dopravním , vesmírném a lékařském softwarovém průmyslu.

Ocenění

S Patrickem Cousotem získala v roce 2013 cenu ACM SIGPLAN Programming Languages ​​Achievement Award a IEEE Computer Society IEEE Computer Society Harlan D. Mills v roce 2014 za „vynález„ abstraktní interpretace “, rozvoj podpory nástrojů a její praktické použití“ .

Radhia Cousot cena za nejlepší mladý výzkumný pracovník

Od září 2014 cenu za nejlepšího mladého výzkumného pracovníka Radhia Cousot každoročně uděluje programová předsedkyně jménem programového výboru Symposia statické analýzy (SAS).

  • 2014 ( Mnichov , Německo ): Aleksandar Chakarov (University of Colorado, Boulder, CO, USA), očekávané invarianty pro pravděpodobnostní programové smyčky jako pevné body (se Sriramem Sankaranarayananem), M. Müller-Olm & H. Seidl (Eds.): SAS 2014 , LNCS 8723 , str. 85–100, Springer
  • 2015 ( Saint Malo , Francie ): Marianna Rapoport (University of Waterloo, Ontario, Kanada), Precise Data Flow Analysis in the Presence of Correlated Method Calls , (s Ondrejem Lhotákem a Frankem Tipem), S. Blazy & T. Jensen (Eds .): SAS 2015 , LNCS 9291 , s. 54–71, Springer
  • 2016 ( Edinburgh , Skotsko ): Stefan Schulze Frielinghaus (Technische Universität München, Německo), Enforcing Termination of Interprocedural Analysis , (s Helmutem Seidlem a Ralfem Voglerem), Xavier Rival (ed.): SAS 2016 , LNCS 9837 , s. 447– 468, Springer
  • 2017 ( New York , NY, USA ): Suvam Mukherjee (Indický vědecký institut, Bangalore, Indie) a Oded Padon (Tel Avivská univerzita, Izrael), Sémantika místních vláken a její efektivní sekvenční abstrakce pro programy bez rasy , (s Sharon Shoham, Deepak D'Souza a Noam Rinetzky), Francesco Ranzato (ed.): SAS 2017 , LNCS 10422 , pp 253–276 , Springer

Poznámky

Reference

externí odkazy