Питер Ойерн - Википедия - Peter OHearn

Питер О'Хирн

ФРС FREng
Королевское общество Питера О'Хирна.jpg
Питер О'Хирн в Королевское общество день приема в Лондоне, июль 2018 г.
Родившийся
Питер Уильям О'Хирн

07 (1963) (возраст57)
Галифакс, Новая Шотландия, Канада
НациональностьБританский, канадский
ГражданствоСоединенное Королевство, Канада
Альма-матерУниверситет Далхаузи (Бакалавр)
Королевский университет (Магистр, доктор философии)
ИзвестенЛогика разделения[1]
Сгруппированная логика[2]
Статический анализатор Infer[3]
Награды
Научная карьера
ПоляЯзыки программирования[12]
Анализ программы
Формальная проверка
Теоретическая информатика[12]
УчрежденияFacebook
Университетский колледж Лондона
Лондонский университет королевы Марии
Сиракузский университет
ТезисСемантика невмешательства: естественный подход  (1992)
ДокторантРоберт Д. Теннент[13]
ВлиянияДжон С. Рейнольдс[14]
Интернет сайтwww0.cs.ucl.ac.Великобритания/сотрудники/п.ohearn/

Питер Уильям О'Хирн ФРС FREng[7][9] (родился 13 июля 1963 г. в г. Галифакс, Новая Шотландия ) - научный сотрудник Facebook[15] и Профессор из Информатика в Университетский колледж Лондона (UCL).[16] Он внес значительный вклад в формальные методы для корректности программы. В последние годы эти достижения были использованы при разработке промышленных программных инструментов, которые проводят автоматический анализ крупных промышленных кодовых баз.[12]

Образование

О'Хирн получил степень бакалавра компьютерных наук в Университет Далхаузи, Галифакс, Новая Шотландия (1985 г.), за которыми следуют степени магистра (1987 г.) и доктора наук (1991 г.) от Королевский университет, Кингстон, Онтарио, Канада. Его диссертация была на Семантика невмешательства: естественный подходпод руководством Роберта Д. Теннента.[13][17]

Карьера и исследования

О'Хирн известен прежде всего логика разделения,[1] теория, которую он разработал с Джон С. Рейнольдс это открыло новые области для масштабирования логических рассуждений о коде. Это основано на предшествующем исследовании логики ресурсов, проведенном О'Хирном и Дэвидом Пимом. связная логика.[2] Со Стивеном Бруксом, Университет Карнеги Меллон, О'Хирн создал логику параллельного разделения (CSL), расширив теорию. Тони Хоар, обсуждая грандиозную проблему верификации программ, описал CSL как «решение двух проблем ... согласованности и объектной ориентации».[18] [19]

Он провел исследование языков программирования, похожих на АЛГОЛ со своим бывшим научным руководителем Робертом Д. Теннентом, которая стала книгой Алголо-подобные языки.[20]

Логика разделения породила Статический анализатор Infer (Facebook Infer), а статический анализ программы Утилита, разработанная командой О'Хирна в Facebook.[3] Проработав более 20 лет в академических кругах, О'Хирн начал работать в Facebook в 2013 году с приобретением Monoidics Ltd, стартапа, который он основал.[21] С момента своего создания Infer позволил инженерам Facebook устранить десятки тысяч ошибок еще до того, как перейти в производство.[22] Он был открыт в 2016 году и используется Amazon Inc, Spotify, Mozilla, Убер, и другие.[3] В 2017 году О'Хирн и его команда открыли исходный код RacerD, автоматизированного инструмента обнаружения статических состояний гонки, который сокращает время, необходимое для выявления потенциальных проблем в параллельном программном обеспечении, как часть платформы Infer.[23]

О'Хирн был доцентом в Сиракузский университет, Нью-Йорк, США, с 1990 по 1995 год. читатель в информатике в Лондонский университет королевы Марии с 1996 по 1999 год, а затем полный профессор Королевы Марии до своего переезда в Университетский колледж Лондона. В UCL ему было предоставлено кресло, спонсируемое Королевская инженерная академия и Microsoft Research.[24] В 1997 году он был приглашенным ученым в Университет Карнеги Меллон а в 2006 году он был приглашенным исследователем в Microsoft Research Кембридж.[17] Сейчас он работает научным сотрудником в Facebook и профессором в UCL.

Награды и награды

В 2007 году О'Хирн получил Премия Королевского общества за заслуги перед исследованием Вольфсона.[7] В 2011 году О'Хирн и Самин Иштиак были удостоены награды «Самая влиятельная газета POPL».[11] Со Стивеном Бруксом, Университет Карнеги Меллон, он был соучредителем конкурса 2016 г. Премия Гёделя, за изобретение логики параллельного разделения.[8] Также в 2016 году он был избран Член Королевской инженерной академии (FREng) и стал одним из лауреатов ежегодной премии CAV (Computer Aided Verification).[9][10] В 2018 году он был избран Член Королевского общества (ФРС) и награжден Почетной грамотой Доктор юридических наук из Университет Далхаузи.[6][7][5]. В январе 2019 года О'Хирн был удостоен еще одной награды за самую влиятельную бумагу POPL, которую он разделил с тремя коллегами.[4]

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

  1. ^ а б Рейнольдс, Джон С. (2002). «Логика разделения: логика для общих изменяемых структур данных» (PDF). LICS.
  2. ^ а б О'Хирн, П. У .; Пим, Д. Дж. (Июнь 1999 г.). «Логика сгруппированных следствий». Бюллетень символической логики. 5 (2): 215–244. Дои:10.2307/421090. JSTOR  421090. S2CID  2948552.
  3. ^ а б c «Сделать вывод статического анализатора». fbinfer.com.
  4. ^ а б «Премия POPL 2019 за наиболее влиятельную бумагу за исследования, которые привели к выводу Facebook Infer». Facebook. 17 января 2019.
  5. ^ а б https://www.dal.ca/news/2018/04/19/introduction-dal-s-honorary-degree-recipients-for-spring-convocat.html
  6. ^ а б «Выдающиеся ученые, избранные научными сотрудниками и иностранными членами Королевского общества». royalsociety.org. Получено 15 мая 2018.
  7. ^ а б c d е Анон (2018). "Профессор Питер О'Хирн FRS". royalsociety.org. Лондон: Королевское общество. Архивировано из оригинал 7 июня 2018 г. Одно или несколько предыдущих предложений включают текст с веб-сайта royalsociety.org, где:

    «Весь текст, опубликованный под заголовком« Биография »на страницах профиля участника, доступен в Международная лицензия Creative Commons Attribution 4.0.” --«Архивная копия». Архивировано 11 ноября 2016 года.. Получено 7 июн 2018.CS1 maint: заархивированная копия как заголовок (связь) CS1 maint: BOT: статус исходного URL-адреса неизвестен (связь)

  8. ^ а б Чита, Эфи (12–15 июля 2016 г.). «Премия Гёделя 2016 года». Европейская ассоциация теоретической информатики.
  9. ^ а б c https://www.raeng.org.uk/about-us/the-fellowship/new-fellows-2016/fellows/peter-o-hearn
  10. ^ а б О'Салливан, Брайан (5 сентября 2016 г.). «Четыре сотрудника Facebook выиграли престижную награду CAV». Facebook.
  11. ^ а б «Профессор информатики получил престижную награду». Лондонский университет королевы Марии. 3 февраля 2011 г.
  12. ^ а б c Питер О'Хирн публикации, проиндексированные Google ученый Отредактируйте это в Викиданных
  13. ^ а б Питер О'Хирн на Проект "Математическая генеалогия" Отредактируйте это в Викиданных
  14. ^ Оливье Дэнви, Питер О'Хирн и Филип Вадлер (редакторы), Festschrift к 70-летию Джона К. Рейнольдса. Теоретическая информатика, 375 (1–3): 1–350, 1 мая 2007 г. От редакции, страницы 1–2.Дои:10.1016 / j.tcs.2006.12.024
  15. ^ "Питер О'Хирн". Facebook исследования.
  16. ^ "Питер О'Хирн". www0.cs.ucl.ac.uk.
  17. ^ а б Питер У. О'Хирн, биография В архиве 2011-07-19 на Wayback Machine, Королева Мэри, Лондонский университет, ВЕЛИКОБРИТАНИЯ.
  18. ^ https://www.facebook.com/academics/videos/2228616734102290/?t=3775
  19. ^ Хоар, Тони (2003). «Проверяющий компилятор». Журнал ACM. 50: 63–69. Дои:10.1145/602382.602403. S2CID  441648.
  20. ^ О'Хирн, Питер; Теннент, Роберт Д. (1997). Алголо-подобные языки. Кембридж, Массачусетс, США: Birkhauser Boston. Дои:10.1007/978-1-4612-4118-8. ISBN  978-0-8176-3880-1. S2CID  6273486.
  21. ^ «Facebook приобретает активы британского разработчика программного обеспечения для проверки мобильных ошибок Monoidics». TechCrunch. Verizon Media.
  22. ^ «Непрерывное рассуждение: масштабирование воздействия формальных методов». Facebook исследования.
  23. ^ «Facebook с открытым исходным кодом RacerD: инструмент, который уже устранил 1000 ошибок в параллельном коде». TechRepublic. 19 октября 2017.
  24. ^ "Весенний вестник" (PDF). raeng.org.uk. 2012.

Эта статья включает текст доступно под CC BY 4.0 лицензия.