Радия Кузо — французский учёный в области информатики, известная изобретением метода абстрактной интерпретации компьютерных программ. Абстрактная интерпретация позволяет делать выводы о семантике (поведении) программ, не запуская её полностью, но используя заложенные в ней алгоритмические свойства с помощью анализа потока управления и потока данных. Таким образом, абстрактная интерпретация плотно связана с такими подходами, как суперкомпиляция В. Ф. Турчина, частичные вычисления Ё. Футамуры и смешанные вычисления А. П. Ершова. Методы статического анализа кода современной информатики немыслимы без абстрактной интерпретации.
Биография
Радия Кузо родилась в Тунисе, в городе Сакет-Сиди-Юсеф. В возрасте десяти лет этот город разбомбила французская армия в ответ на сбитый в алжирской войне за независимость самолёт. В результате налёта было убито 75 местных жителей и 150 ранено, но Кузо не пострадала. После лицея в Сусе и затем в Алжире она поступила в престижную Политехническую школу Алжира, которую закончила с отличием. Благодаря гранту ЮНЕСКО, она получила шанс закончить магистратуру в Университете Гренобля в 1972. В 1985 в Нанси она защитила кандидатскую диссертацию по теме «Основы методов доказательства инвариантности и конечности параллельных программ» (фр. Fondements des mthodes de preuve d'invariance et de fatalit de programmes parallles).
Места работы Радии Кузо включали:
- Университет Гренобль 1 — стипендиат ЮНЕСКО (1971—1974), адъюнкт (1975—1979)
- Национальный центр научных исследований
- Университет Нанси I — младший научный сотрудник (1980—1983)
- Университет Париж-юг XI — научный сотрудник (1983—1988)
- Политехническая школа — научный сотрудник (1989—1995), старший научный сотрудник (1996—2008)
- Высшая нормальная школа — старший научный сотрудник (2006—2014)
- IBM Research Thomas J. Watson Research Center — приглашённый учёный (2006, 2007)
- Microsoft Research — приглашённый учёный (2009, 2010, 2011)
Радия Кузо скончалась 1 мая 2014 в Нью-Йорке от рака желудочно-кишечного тракта.
Научные достижения
Абстрактная интерпретация — техника, предложенная Радией и Патриком Кузо в конце 1970-х, оказала большое влияние на развитие формальных методов. Она основана на трёх идеях:
- Любое рассуждение, доказательство или статический анализ компьютерной системы опирается на семантику, описывающую, на каком-то уровне абстракции, её возможные варианты выполнения.
- Рассуждение, доказательство или статический анализ должен абстрагироваться от всех семантических свойств, не имеющих отношение к аргументации.
- В доказательствах допустимы приблизительные выводы с помощью математической индукции, посколько точные могут быть недостижимы из-за принципиальной нерешаемости, невозможности автоматизации или комбинаторного взрыва.
В диссертации Радия Кузо предложила формализацию семантики, схемы доказательств и методы статического анализа для конкурентных и параллельных программ
В 2013 Радия и Патрик Кузо получили награду ACM SIGPLAN Programming Languages Achievement Award за достижения в теории языков программирования и аналогичную награду IEEE Computer Society Harlan Mills Award «за изобретение абстрактной интерпретации, разработку программного обеспечения и практическое их применение». В сентябре 2014, через несколько месяцев после смерти Кузо, была учреждена награда её имени для поощрения молодых учёных, вручаемая ежегодно на симпозиуме по статическому анализу (Static Analysis Symposium, SAS) за лучшую статью, представленную молодым учёным. Получателями первых лет стали:
- (2014) Александар Чакаров (Колорадский университет в Боулдере, США)
- (2015) Марианна Рапопорт (Университет Ватерлоо, Канада)
- (2016) Штефан Шульце Фрилингау (Технический университет Мюнхена, Германия)
Ссылки
- Домашняя страница Радии Кузо на последнем месте работы
- Биография
- Список публикаций
- Награда Радии Кузо
- Disparition de Radhia Cousot
- Radhia Cousot на DBLP (список статей)
- Кузо, Радия (англ.) в проекте «Математическая генеалогия»
