Кузо, Радия: различия между версиями

Материал из Википедии — свободной энциклопедии
Перейти к навигации Перейти к поиску
Интерактивная навигация по истории
[отпатрулированная версия][отпатрулированная версия]
← Предыдущая правкаСледующая правка →
Содержимое удалено Содержимое добавлено
ВизуальныйВики-текст
Спасено источников — 1, отмечено мёртвыми — 0. #IABot (v1.6beta3)
м орфография
Строка 43: Строка 43:
# Любое рассуждение, доказательство или статический анализ компьютерной системы опирается на семантику, описывающую, на каком-то уровне абстракции, её возможные варианты выполнения.
# Любое рассуждение, доказательство или статический анализ компьютерной системы опирается на семантику, описывающую, на каком-то уровне абстракции, её возможные варианты выполнения.
# Рассуждение, доказательство или статический анализ должен абстрагироваться от всех семантических свойств, не имеющих отношение к аргументации.
# Рассуждение, доказательство или статический анализ должен абстрагироваться от всех семантических свойств, не имеющих отношение к аргументации.
# В доказательствах допустимы приблизительные выводы с помощью математической индукции, посколько точные могут быть недостижимы из-за принципиальной нерешаемости, невозможности автоматизации или комбинаторного взрыва.
# В доказательствах допустимы приблизительные выводы с помощью математической индукции, поскольку точные могут быть недостижимы из-за принципиальной нерешаемости, невозможности автоматизации или комбинаторного взрыва.


В диссертации Радия Кузо предложила [[формальная семантика|формализацию семантики]], схемы [[математическое доказательство|доказательств]] и методы [[статический анализ кода|статического анализа]] для [[конкурентные вычисления|конкурентных]] и [[параллельные вычисления|параллельных]] программ<ref>Radhia Cousot, [http://www.di.ens.fr/~rcousot/COUSOTpapers/THESE-RC-1985.shtml Fondements des méthodes de preuve d’invariance et de fatalité de programmes parallèles]. Thèse ès Sciences Mathématiques, Institut national polytechnique de Lorraine, Nancy, France, 15 November 1985.</ref>
В диссертации Радия Кузо предложила [[формальная семантика|формализацию семантики]], схемы [[математическое доказательство|доказательств]] и методы [[статический анализ кода|статического анализа]] для [[конкурентные вычисления|конкурентных]] и [[параллельные вычисления|параллельных]] программ<ref>Radhia Cousot, [http://www.di.ens.fr/~rcousot/COUSOTpapers/THESE-RC-1985.shtml Fondements des méthodes de preuve d’invariance et de fatalité de programmes parallèles]. Thèse ès Sciences Mathématiques, Institut national polytechnique de Lorraine, Nancy, France, 15 November 1985.</ref>

Версия от 18:05, 13 января 2019

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

ACM SIGPLAN Programming Languages Achievement Award

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

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

Биография

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

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

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

Научные достижения

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

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

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

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

Ссылки

Примечания

  1. ↑ 1 2 3 4 Fichier des personnes décédées
  2. ↑ 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.
  3. ↑ 1 2 Patrick Cousot, Radhia Cousot, «Systematic Design of Program Analysis Frameworks», POPL, 1979.
  4. ↑ Michael Leuschel, «A Framework for the Integration of Partial Evaluation and Abstract Interpretation of Logic Programs», ACM TOPLAS, 2004.
  5. ↑ Radhia Cousot на Mathematics Genealogy Project.
  6. ↑ Curriculum Vitae, 2011, Radhia Cousot.
  7. ↑ Radhia Cousot — Short biography
  8. ↑ Radhia Cousot, Fondements des méthodes de preuve d’invariance et de fatalité de programmes parallèles. Thèse ès Sciences Mathématiques, Institut national polytechnique de Lorraine, Nancy, France, 15 November 1985.
  9. ↑ ACM SIGPLAN Programming Languages Achievement Award Архивировано 18 мая 2014 года.
  10. ↑ IEEE Computer Society Harlan D. Mills
  11. ↑ Static Analysis Symposia (SAS)
  12. ↑ Radhia Cousot best young researcher paper award
Источник — https://ru.wikipedia.org/ruwiki/w/index.php?title=Кузо,_Радия&oldid=97452888