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

Радия Кузо
RadhiaCousot - Picture.jpg
Родившийся(1947-08-06)6 августа 1947 г.
Сакьет Сиди Юсеф, Тунис
Умер1 мая 2014 г.(2014-05-01) (67 лет)
Нью-Йорк
НациональностьФранцузский
Альма-матерInstitut National Polytechnique de Lorraine
ИзвестенАбстрактная интерпретация
Супруг (а)Патрик Кузо
НаградыACM СИГПЛАН Премия за достижения в области языков программирования
IEEE Computer Society Премия Харлана Д. Миллса
Научная карьера
ПоляИнформатика
ТезисФонд методов обеспечения инвариантности и фатальности параллельных программ (1985)
ДокторантКлод Пара

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

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

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

Карьера

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

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

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

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

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

Радия Кузо стоит у истоков контактов с Airbus в январе 1999 г., что привело к развитию Анализатор ошибок времени выполнения Astrée с 2001 г. инструмент для звука статический анализ программы из встроенныйконтроль / команда программного обеспечения разработан в École Normale Supérieure[5] и теперь распространяется AbsInt GmbH,[6] немецкая софтверная компания, специализирующаяся на статическом анализе. Astrée используется в транспорт, Космос, и медицинский программное обеспечение.

Награды

С Патрик Кузо, она получила ACM Премия SIGPLAN Programming Languages ​​Achievement Award [7] в 2013 году и IEEE Computer Society Компьютерное общество IEEE Харлан Д. Миллс награда [8] в 2014 году за «изобретение»абстрактная интерпретация ’, Разработка инструментального обеспечения и его практическое применение».

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

С сентября 2014 г. Премия Радии Кусо за лучшую работу молодых исследователей[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–468, Springer
  • 2017 (Нью-Йорк, Нью-Йорк, США ): Сувам Мукерджи (Индийский институт науки, Бангалор, Индия) и Одед Падон (Тель-Авивский университет, Израиль), Локальная по потоку семантика и ее эффективные последовательные абстракции для программ без расы, (с Шэрон Шохам, Дипак Д'Суза и Ноам Ринецки), Франческо Ранзато (ред.): SAS 2017, LNCS 10422, стр. 253–276, Springer

Примечания

  1. ^ В 1980-х годах во Франции существовало два уровня докторантуры: более высокий и Doctorate ès Sciences / Государственный доктор необходимо для доступа профессуры. С тех пор он был заменен на абилитация.

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

  1. ^ "Institut des Sciences de l'information et de leurs взаимодействия - CNRS - Disparition de Radhia Cousot". www.cnrs.fr.
  2. ^ Кузо, Патрик; Кузо, Радия (1 января 1977 г.). «Абстрактная интерпретация». Абстрактная интерпретация: единая решетчатая модель для статического анализа программ путем построения или аппроксимации фиксированных точек.. ACM. С. 238–252. CiteSeerX  10.1.1.216.8213. Дои:10.1145/512950.512973 - через dl.acm.org.
  3. ^ Кузо, Патрик; Кузо, Радия (1 января 1979 г.). «Систематическое проектирование структур программного анализа». Материалы 6-го симпозиума ACM SIGACT-SIGPLAN по принципам языков программирования - POPL '79. ACM. С. 269–282. CiteSeerX  10.1.1.207.2895. Дои:10.1145/567752.567778 - через dl.acm.org.
  4. ^ "Р. Кузо, Фонд методов борьбы с изменчивостью и фаталитизма параллельных программ". www.di.ens.fr.
  5. ^ "Домашняя страница статического анализатора Astrée в ENS". Ens.fr.
  6. ^ [email protected]. «Анализатор ошибок времени выполнения Astrée». www.absint.com.
  7. ^ «Премия за достижения в области языков программирования». www.sigplan.org.
  8. ^ «Премия Харлана Д. Миллса • Компьютерное общество IEEE». www.computer.org.
  9. ^ https://www.di.ens.fr/~rcousot/, Радия Кузо. «Премия Радии Кусо за лучшую работу молодых исследователей». www.di.ens.fr.
  10. ^ "Центральный сайт симпозиумов по статическому анализу". staticanalysis.org.

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