Радия Кузо - Radhia Cousot

Радия Кузо
RadhiaCousot - Picture.jpg
Родившийся ( 1947-08-06 ) 6 августа 1947 г.
Умер 1 мая 2014 г. (2014-05-01) (67 лет)
Национальность Французский
Альма-матер Institut National Polytechnique de Lorraine
Известен Абстрактная интерпретация
Супруг (а) Патрик Кузо
Награды ACM SIGPLAN Премия за достижения в области языков программирования
IEEE Computer Society Премия Харлана Д. Миллса
Научная карьера
Поля Информатика
Тезис Fondements des méthodes de preuve d'invariance et de fatalité de program parallèles   (1985)
Докторант Клод Пара

Радия Кузо (6 августа 1947 - 1 мая 2014) была французским ученым-компьютерщиком, известным изобретением абстрактной интерпретации .

Исследования

Радия Кусо родилась 6 августа 1947 года в городе Сакиет Сиди Юсеф в Тунисе , где она пережила массовое убийство детей в своей школе 8 февраля 1958 года . Затем она пошла в Lycée de jeunes filles в Суссе , в Lycée français в Алжире, а затем в Политехническую школу Алжира (где она заняла 1-е место и была единственной женщиной). Она специализировалась на математической оптимизации и целочисленном линейном программировании . Поддерживается ЮНЕСКО стипендий (1972-1975), она получила степень магистра в области компьютерных наук ( Diplôme д'этюд approfondies (DEA) ) на Джозефа Фурье университета в Гренобле в 1972 г. Она получила докторскую степень ÉS Sciences / Государственный Докторантуру в математике в Нэнси в 1985 году под руководством Клода Пэра  [ фр ] .

Карьера

Радия Кузо была назначена младшим научным сотрудником лаборатории IMAG Университета Джозефа Фурье в Гренобле (1975–1979), а с 1980 года - в Национальном центре научных исследований в качестве младшего научного сотрудника, научного сотрудника, старшего научного сотрудника. и старший научный сотрудник лабораторий компьютерных наук Университета Анри Пуанкаре в Нанси (1980–1983), Университета Париж-Юг в Орсе (1984–1988), Политехнической школы (1989–2008), где с 1991 года она возглавляла исследовательская группа «Семантика, доказательство и абстрактная интерпретация» и Высшая нормальная школа (2006–2014).

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

Вместе со своим мужем Патриком Радия Кузо является создателем абстрактной интерпретации , влиятельной техники в формальных методах . Абстрактная интерпретация основана на трех основных идеях.

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

В своей диссертации Радия Кузо усовершенствовала методы семантики, доказательства и статического анализа для параллельных и параллельных программ.

Радхия Каусот находится в начале контактов с Airbus в январе 1999 года , что привело к развитию Astrée времени выполнения анализатора ошибок начиная с 2001 года, инструмент для звукового анализа статической программы из встроенного контроля / управления программного обеспечения , разработанного в Эколь Нормаль Supérieure и теперь распространяется AbsInt GmbH , немецкой компанией-разработчиком программного обеспечения, специализирующейся на статическом анализе. Astrée используется в транспортной , космической и медицинской отраслях программного обеспечения.

Награды

Вместе с Патриком Кузо она получила премию ACM SIGPLAN Programming Languages ​​Achievement Award в 2013 году и награду IEEE Computer Society Harlan D. Mills в 2014 году за «изобретение« абстрактной интерпретации », разработку поддержки инструментов и ее практическое применение». .

Премия Радии Кузо за лучшую работу молодых исследователей

С сентября 2014 года награда Radhia Cousot за лучшую работу молодого исследователя ежегодно присуждается председателем программы от имени программного комитета Симпозиумов по статическому анализу (SAS).

  • 2014 ( Мюнхен , Германия ): Александр Чакаров (Университет Колорадо, Боулдер, Колорадо, США), Инварианты ожидания для вероятностных программных циклов как фиксированных точек (со Шрирамом Санкаранараянаном), М. Мюллер-Олм и Х. Зайдл (ред.): SAS 2014 , LNCS 8723 , стр. 85–100, Springer
  • 2015 ( Сен-Мало , Франция ): Марианна Рапопорт (Университет Ватерлоо, Онтарио, Канада), Точный анализ потока данных при наличии коррелированных вызовов методов (с Ондреем Лхотаком и Фрэнком Типом), С. Блейзи и Т. Йенсен (редакторы .): SAS 2015 , LNCS 9291 , стр. 54–71, Springer.
  • 2016 ( Эдинбург , Шотландия ): Stefan Schulze Frielinghaus (Technische Universität München, Германия), Принудительное прекращение межпроцедурного анализа , (с Гельмутом Зайдлом и Ральфом Фоглером), Ксавье Ривал (ред.): SAS 2016 , LNCS 9837 , стр. 447–447. 468, Springer
  • 2017 ( Нью-Йорк , Нью-Йорк, США ): Сувам Мукерджи (Индийский институт науки, Бангалор, Индия) и Одед Падон (Тель-Авивский университет, Израиль), Локальная семантика потоков и ее эффективные последовательные абстракции для программ , свободных от расы , (с Шарон Шохам, Дипак Д'Суза и Ноам Ринецки), Франческо Ранзато (ред.): SAS 2017 , LNCS 10422 , стр. 253–276, Springer.

Примечания

Рекомендации

внешняя ссылка