Кузо, Радия

Материал из Википедии — свободной энциклопедии
Перейти к навигации Перейти к поиску
Радия Кузо
Radhia Cousot
Имя при рождении фр. Radhia Rezig[1]
Дата рождения 6 августа 1947(1947-08-06)[1]
Место рождения
Дата смерти 1 мая 2014(2014-05-01)[1] (66 лет)
Место смерти
Страна Франция
Научная сфера информатика
Место работы Университет Гренобль 1
Национальный центр научных исследований
Университет Нанси I
Университет Париж-юг XI
Политехническая школа
Высшая нормальная школа
Альма-матер Institut National Polytechnique de Lorraine
Учёная степень доктор философии
Учёное звание профессор
Научный руководитель Клод Пэр[fr]
Известна как соавтор абстрактной интерпретации
Награды и премии

ACM SIGPLAN Programming Languages Achievement Award

IEEE Computer Society Harlan D. Mills Award
Логотип Викисклада Медиафайлы на Викискладе

Радия Кузо (6 августа 1947 — 1 мая 2014[2]) — французский учёный в области информатики, известная изобретением метода абстрактной интерпретации[en] компьютерных программ. Абстрактная интерпретация позволяет делать выводы о семантике (поведении) программ, не запуская её полностью, но используя заложенные в ней алгоритмические свойства с помощью анализа потока управления и потока данных[en][3][4]. Таким образом, абстрактная интерпретация плотно связана с такими подходами, как суперкомпиляция В. Ф. Турчина, частичные вычисления Ё. Футамуры и смешанные вычисления А. П. Ершова[5]. Методы статического анализа кода современной информатики немыслимы без абстрактной интерпретации.

Биография[править | править код]

Радия Кузо родилась в Тунисе, в городе Сакет-Сиди-Юсеф[en]. В возрасте десяти лет этот город разбомбила французская армия[fr] в ответ на сбитый в алжирской войне за независимость самолёт. В результате налёта было убито 75 местных жителей и 150 ранено, но Кузо не пострадала. После лицея в Сусе и затем в Алжире она поступила в престижную Политехническую школу Алжира[en], которую окончила с отличием. Благодаря гранту ЮНЕСКО, она получила шанс закончить магистратуру в Университете Гренобля в 1972. В 1985 в Нанси она защитила кандидатскую диссертацию по теме «Основы методов доказательства инвариантности и конечности[en] параллельных программ» (фр. Fondements des méthodes de preuve d'invariance et de fatalité de programmes parallèles)[6].

Места работы Радии Кузо включали[7]:

Радия Кузо скончалась 1 мая 2014 в Нью-Йорке от рака желудочно-кишечного тракта[8].

Научные достижения[править | править код]

Абстрактная интерпретация — техника, предложенная Радией и Патриком Кузо в конце 1970-х[3][4], оказала большое влияние на развитие формальных методов. Она основана на трёх идеях:

  1. Любое рассуждение, доказательство или статический анализ компьютерной системы опирается на семантику, описывающую, на каком-то уровне абстракции, её возможные варианты выполнения.
  2. Рассуждение, доказательство или статический анализ должен абстрагироваться от всех семантических свойств, не имеющих отношение к аргументации.
  3. В доказательствах допустимы приблизительные выводы с помощью математической индукции, поскольку точные могут быть недостижимы из-за принципиальной нерешаемости, невозможности автоматизации или комбинаторного взрыва.

В диссертации Радия Кузо предложила формализацию семантики, схемы доказательств и методы статического анализа для конкурентных и параллельных программ[9]

В 2013 Радия и Патрик Кузо получили награду ACM SIGPLAN[en] Programming Languages Achievement Award[10] за достижения в теории языков программирования и аналогичную награду IEEE Computer Society[en] Harlan Mills[en] Award[11] «за изобретение абстрактной интерпретации, разработку программного обеспечения и практическое их применение». В сентябре 2014, через несколько месяцев после смерти Кузо, была учреждена награда её имени для поощрения молодых учёных, вручаемая ежегодно на симпозиуме по статическому анализу (Static Analysis Symposium, SAS)[12] за лучшую статью, представленную молодым учёным. Получателями первых лет стали[13]:

Примечания[править | править код]

  1. 1 2 3 4 Fichier des personnes décédées
  2. Institut des sciences de l'information et de leurs interactions - CNRS - Disparition de Radhia Cousot. www.cnrs.fr. Дата обращения: 3 декабря 2016. Архивировано 4 января 2017 года.
  3. 1 2 Patrick Cousot, Radhia Cousot, «Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints», POPL, 1977.
  4. 1 2 Patrick Cousot, Radhia Cousot, «Systematic Design of Program Analysis Frameworks», POPL, 1979.
  5. Michael Leuschel, «A Framework for the Integration of Partial Evaluation and Abstract Interpretation of Logic Programs», ACM TOPLAS, 2004.
  6. Radhia Cousot Архивная копия от 8 июня 2017 на Wayback Machine на Mathematics Genealogy Project.
  7. Curriculum Vitae, 2011, Radhia Cousot Архивная копия от 21 июня 2015 на Wayback Machine.
  8. Radhia Cousot — Short biography. Дата обращения: 3 декабря 2016. Архивировано из оригинала 15 августа 2016 года.
  9. Radhia Cousot, Fondements des méthodes de preuve d’invariance et de fatalité de programmes parallèles Архивная копия от 23 сентября 2015 на Wayback Machine. Thèse ès Sciences Mathématiques, Institut national polytechnique de Lorraine, Nancy, France, 15 November 1985.
  10. ACM SIGPLAN Programming Languages Achievement Award Архивировано 18 мая 2014 года.
  11. IEEE Computer Society Harlan D. Mills. Дата обращения: 3 декабря 2016. Архивировано из оригинала 10 января 2011 года.
  12. Static Analysis Symposia (SAS). Дата обращения: 3 декабря 2016. Архивировано 18 ноября 2016 года.
  13. Radhia Cousot best young researcher paper award. Дата обращения: 3 декабря 2016. Архивировано из оригинала 23 января 2017 года.

Ссылки[править | править код]