Русская Википедия:Кузо, Радия
Шаблон:Учёный Радия Кузо (6 августа 1947 — 1 мая 2014[1]) — французский учёный в области информатики, известная изобретением метода Шаблон:Нп5 компьютерных программ. Абстрактная интерпретация позволяет делать выводы о семантике (поведении) программ, не запуская её полностью, но используя заложенные в ней алгоритмические свойства с помощью анализа потока управления и Шаблон:Нп5[2][3]. Таким образом, абстрактная интерпретация плотно связана с такими подходами, как суперкомпиляция В. Ф. Турчина, частичные вычисления Ё. Футамуры и смешанные вычисления А. П. Ершова[4]. Методы статического анализа кода современной информатики немыслимы без абстрактной интерпретации.
Биография
Радия Кузо родилась в Тунисе, в городе Шаблон:Нп5. В возрасте десяти лет этот город Шаблон:Нп5 в ответ на сбитый в алжирской войне за независимость самолёт. В результате налёта было убито 75 местных жителей и 150 ранено, но Кузо не пострадала. После лицея в Сусе и затем в Алжире она поступила в престижную Шаблон:Нп5, которую окончила с отличием. Благодаря гранту ЮНЕСКО, она получила шанс закончить магистратуру в Университете Гренобля в 1972. В 1985 в Нанси она защитила кандидатскую диссертацию по теме «Основы методов доказательства инвариантности и Шаблон:Нп5 параллельных программ» (Шаблон:Lang-fr)[5].
Места работы Радии Кузо включали[6]:
- Университет Гренобль 1 — стипендиат ЮНЕСКО (1971—1974), адъюнкт (1975—1979)
- Национальный центр научных исследований
- Университет Нанси I — младший научный сотрудник (1980—1983)
- Университет Париж-юг XI — научный сотрудник (1983—1988)
- Политехническая школа — научный сотрудник (1989—1995), старший научный сотрудник (1996—2008)
- Высшая нормальная школа — старший научный сотрудник (2006—2014)
- Шаблон:Нп5 Шаблон:Нп5 — приглашённый учёный (2006, 2007)
- Microsoft Research — приглашённый учёный (2009, 2010, 2011)
Радия Кузо скончалась 1 мая 2014 в Нью-Йорке от рака желудочно-кишечного тракта[7].
Научные достижения
Абстрактная интерпретация — техника, предложенная Радией и Патриком Кузо в конце 1970-х[2][3], оказала большое влияние на развитие формальных методов. Она основана на трёх идеях:
- Любое рассуждение, доказательство или статический анализ компьютерной системы опирается на семантику, описывающую, на каком-то уровне абстракции, её возможные варианты выполнения.
- Рассуждение, доказательство или статический анализ должен абстрагироваться от всех семантических свойств, не имеющих отношение к аргументации.
- В доказательствах допустимы приблизительные выводы с помощью математической индукции, поскольку точные могут быть недостижимы из-за принципиальной нерешаемости, невозможности автоматизации или комбинаторного взрыва.
В диссертации Радия Кузо предложила формализацию семантики, схемы доказательств и методы статического анализа для конкурентных и параллельных программ[8]
В 2013 Радия и Патрик Кузо получили награду ACM Шаблон:Нп5 Programming Languages Achievement Award[9] за достижения в теории языков программирования и аналогичную награду IEEE Шаблон:Нп5 Шаблон:Нп5 Award[10] «за изобретение абстрактной интерпретации, разработку программного обеспечения и практическое их применение». В сентябре 2014, через несколько месяцев после смерти Кузо, была учреждена награда её имени для поощрения молодых учёных, вручаемая ежегодно на симпозиуме по статическому анализу (Static Analysis Symposium, SAS)[11] за лучшую статью, представленную молодым учёным. Получателями первых лет стали[12]:
- (2014) Александар Чакаров (Колорадский университет в Боулдере, США)
- (2015) Марианна Рапопорт (Университет Ватерлоо, Канада)
- (2016) Штефан Шульце Фрилингау (Технический университет Мюнхена, Германия)
Примечания
Ссылки
- Домашняя страница Радии Кузо на последнем месте работы
- Биография
- Список публикаций
- Награда Радии Кузо
- Disparition de Radhia Cousot
- Radhia Cousot на DBLP (список статей)
- Шаблон:MathGenealogy
- ↑ Шаблон:Cite web
- ↑ 2,0 2,1 Patrick Cousot, Radhia Cousot, «Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints», POPL, 1977.
- ↑ 3,0 3,1 Patrick Cousot, Radhia Cousot, «Systematic Design of Program Analysis Frameworks», POPL, 1979.
- ↑ Michael Leuschel, «A Framework for the Integration of Partial Evaluation and Abstract Interpretation of Logic Programs», ACM TOPLAS, 2004.
- ↑ Radhia Cousot Шаблон:Wayback на Mathematics Genealogy Project.
- ↑ Curriculum Vitae, 2011, Radhia Cousot Шаблон:Wayback.
- ↑ Шаблон:Cite web
- ↑ Radhia Cousot, Fondements des méthodes de preuve d’invariance et de fatalité de programmes parallèles Шаблон:Wayback. Thèse ès Sciences Mathématiques, Institut national polytechnique de Lorraine, Nancy, France, 15 November 1985.
- ↑ ACM SIGPLAN Programming Languages Achievement Award Шаблон:Webarchive
- ↑ Шаблон:Cite web
- ↑ Шаблон:Cite web
- ↑ Шаблон:Cite web
