Радия Кузо (6 августа 1947 - 1 мая 2014) [1] была французским ученым-компьютерщиком, известным изобретением абстрактной интерпретации .
Радия Кузо | |
---|---|
Родившийся | |
Умер | 1 мая 2014 г. | (67 лет)
Национальность | Французский |
Альма-матер | Национальный политехнический институт Лотарингии |
Известен | Абстрактная интерпретация |
Супруг (а) | Патрик Кузо |
Награды | ACM SIGPLAN Премия за достижения в области языков программирования IEEE Computer Society Премия Харлана Д. Миллса |
Научная карьера | |
Поля | Информатика |
Тезис | Fondements des méthodes de preuve d'invariance et de fatalité de program parallèles (1985) |
Докторант | Клод Пара |
Исследования
Радия Кусо родилась 6 августа 1947 года в городе Сакьет Сиди Юсеф в Тунисе , где она пережила массовое убийство детей в своей школе 8 февраля 1958 года . Затем она пошла в Lycée de jeunes filles в Суссе , в Lycée français в Алжире, а затем в Политехническую школу Алжира (где она заняла 1-е место и была единственной женщиной). Она специализировалась на математической оптимизации и целочисленном линейном программировании . Поддерживается ЮНЕСКО стипендий (1972-1975), она получила степень магистра в области компьютерных наук ( Diplôme д'этюд approfondies (DEA) ) на Джозефа Фурье университета в Гренобле в 1972 г. Она получила докторскую степень ÉS Sciences / Государственный Докторантуру в математике в Нэнси в 1985 году под руководством Клода Пэра . [nb 1]
Карьера
Радия Кузо была назначена младшим научным сотрудником лаборатории IMAG Университета Джозефа Фурье в Гренобле (1975–1979), а с 1980 года - в Национальном центре научных исследований в качестве младшего научного сотрудника, научного сотрудника, старшего научного сотрудника. и старший научный сотрудник лабораторий компьютерных наук Университета Анри Пуанкаре в Нанси (1980–1983), Университета Париж-Юг в Орсе (1984–1988), Политехнической школы (1989–2008), где с 1991 года она возглавляла исследовательская группа «Семантика, доказательство и абстрактная интерпретация» и Высшая нормальная школа (2006–2014).
Научные достижения
Вместе с мужем Patrick , Радхия Каусот является создателем абстрактной интерпретации , [2] [3] влиятельный метод в формальных методах . Абстрактная интерпретация основана на трех основных идеях.
- Любое рассуждение / доказательство / статический анализ в компьютерной системе относится к семантике, описывающей на некотором уровне абстракции ее возможное выполнение.
- Обоснование / доказательство / статический анализ должны абстрагироваться от всех семантических свойств, не относящихся к рассуждению.
- Из-за неразрешимости , надежных, полностью автоматизированных и всегда заканчивающихся рассуждений о / доказательствах / статическом анализе компьютерных систем математические индукции должны выполняться абстрактно, и поэтому они могут быть только приблизительными (даже с гипотезой конечности и разрешимости, из-за комбинаторного взрыва за пределами крошечного системы).
В своей диссертации Радия Кузо усовершенствовала методы семантики, доказательства и статического анализа для параллельных и параллельных программ. [4]
Радия Кусо была у истоков контактов с Airbus в январе 1999 года, которые привели к разработке с 2001 года анализатора ошибок времени выполнения Astrée , инструмента для надежного статического анализа программ встроенного управляющего / командного программного обеспечения, разработанного в École Normale Supérieure [ 5] и теперь распространяется Absint GmbH , [6] немецкого программного обеспечения компания специализируется на статическом анализе. Astrée используется в транспортной , космической и медицинской отраслях программного обеспечения.
Награды
С Патрик Каусот , она получила ACM SIGPLAN Программирование премии Достижение Языки [7] в 2013 году и IEEE Computer Society IEEE Computer Society Харлан Д. Миллс награду [8] в 2014 году для «изобретения„ абстрактной интерпретации “, разработка инструмента поддержки , и его практическое применение ».
Премия Радии Кузо за лучшую работу молодых исследователей
С сентября 2014 года награда Radhia Cousot за лучшую работу молодого исследователя [9] ежегодно присуждается председателем программы от имени программного комитета Симпозиумов по статическому анализу (SAS). [10]
- 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
Заметки
- ^ В 1980-х годах во Франции существовало два уровня докторантуры, причем на более высоком уровне докторская степень / государственная докторская степень была необходима для доступа к профессорским должностям . С тех пор его заменила абилитация .
Рекомендации
- ^ "Институт наук де л'информации и взаимодействий - CNRS - Disparition de Radhia Cousot" . www.cnrs.fr .
- ^ Кузо, Патрик; Кузо, Радия (1 января 1977 г.). «Абстрактная интерпретация» . Абстрактная интерпретация: единая решетчатая модель для статического анализа программ путем построения или аппроксимации фиксированных точек . ACM. С. 238–252. CiteSeerX 10.1.1.216.8213 . DOI : 10.1145 / 512950.512973 . S2CID 207614632 - через dl.acm.org.
- ^ Кузо, Патрик; Кузо, Радия (1 января 1979 г.). «Систематическое проектирование структур программного анализа» . Материалы 6-го симпозиума ACM SIGACT-SIGPLAN по принципам языков программирования - POPL '79 . ACM. С. 269–282. CiteSeerX 10.1.1.207.2895 . DOI : 10.1145 / 567752.567778 . S2CID 1547466 - через dl.acm.org.
- ^ "R. Cousot, Fondements des méthodes de preuve d'invariance et de fatalité de program parallèles" . www.di.ens.fr .
- ^ "Домашняя страница статического анализатора Astrée в ENS" . ens.fr .
- ^ [email protected]. «Анализатор ошибок времени выполнения Astrée» . www.absint.com .
- ^ «Премия за достижения в области языков программирования» . www.sigplan.org .
- ^ «Премия Харлана Д. Миллса • Компьютерное общество IEEE» . www.computer.org .
- ^ https://www.di.ens.fr/~rcousot/ , Радия Кузо. «Премия Радии Кузо за лучшую работу молодого исследователя» . www.di.ens.fr .
- ^ "Центральный сайт симпозиумов по статическому анализу" . staticanalysis.org .
Внешние ссылки
- Домашняя страница Радии Кузо в Высшей школе нормального образования
- Краткая биография
- Публикации Радии Кузо в École Normale Supérieure
- Награда Радии Кузо в Высшей школе нормального образования
- Де несоответствие Радхия Каусот в Институте де наук De L'информации и др де Leurs взаимодействия по CNRS
- Радия Кузо на сервере библиографии DBLP
- Радия Кузо на проекте « Математическая генеалогия»