stringtranslate.com

Питер О'Херн

Питер Уильям О'Хирн (родился 13 июля 1963 года в Галифаксе, Новая Шотландия ), бывший научный сотрудник в Meta , [15] является выдающимся инженером в Lacework [16] и профессором компьютерных наук в Университетском колледже Лондона (UCL). [17] Он внес значительный вклад в формальные методы корректности программ. В последние годы эти достижения были использованы при разработке промышленных программных инструментов, которые проводят автоматизированный анализ больших промышленных кодовых баз. [10]

Образование

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

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

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

Он провел исследование языков программирования, похожих на ALGOL , совместно со своим бывшим научным руководителем Робертом Д. Теннентом, которое легло в основу книги « Языки, похожие на Algol» . [20]

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

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

Награды и почести

В 2007 году О'Хирн был удостоен премии Вольфсона за исследовательские заслуги Королевского общества . [5] В 2011 году О'Хирн и Самин Иштиак были награждены премией «За самую влиятельную статью POPL». [9] Вместе со Стивеном Бруксом из Университета Карнеги-Меллона он стал соавтором премии Гёделя 2016 года за изобретение логики параллельного разделения. [6] Также в 2016 году он был избран членом Королевской инженерной академии (FREng) и стал одним из обладателей ежегодной премии CAV (Computer Aided Verification). [7] [8] В 2018 году он был избран членом Королевского общества (FRS) и получил звание почетного доктора права от Университета Далхаузи . [4] [5] [3] В январе 2019 года О'Хирн был удостоен еще одной награды «Самая влиятельная статья POPL», которую он разделил с тремя коллегами. [2] Институт инженеров по электротехнике и электронике (IEEE) вручил О'Хирну и трем его коллегам из Facebook премию IEEE Cybersecurity Award for Practice на своей ежегодной церемонии награждения в октябре 2021 года. [1]

Ссылки

  1. ^ ab "Церемония награждения IEEE 2021 - Конференция IEEE по безопасной разработке".
  2. ^ ab «Премия POPL 2019 за самую влиятельную статью за исследование, которое привело к Facebook Infer». Facebook . 17 января 2019 г.
  3. ^ ab "Представляем почетных обладателей степени Даля на весеннем собрании 2018 года".
  4. ^ ab "Выдающиеся ученые, избранные в качестве членов и иностранных членов Королевского общества". royalsociety.org . Получено 15 мая 2018 г. .
  5. ^ abcd Anon (2018). "Профессор Питер О'Херн FRS". royalsociety.org . Лондон: Королевское общество . Архивировано из оригинала 7 июня 2018 года.Одно или несколько из предыдущих предложений включают текст с сайта royalsociety.org, где:

    «Весь текст, опубликованный под заголовком «Биография» на страницах профиля члена, доступен по лицензии Creative Commons Attribution 4.0 International ». — «Условия, положения и политика | Королевское общество». Архивировано из оригинала 11 ноября 2016 г. Получено 7 июня 2018 г.{{cite web}}: CS1 maint: бот: исходный статус URL неизвестен ( ссылка )

  6. ^ ab Chita, Efi (12–15 июля 2016 г.). «Премия Гёделя 2016 г.». Европейская ассоциация теоретической информатики.
  7. ^ ab "Royal Academy Fellows 2016". Архивировано из оригинала 27 марта 2019 года . Получено 26 мая 2018 года .
  8. ^ ab O'Sullivan, Bryan (5 сентября 2016 г.). «Четыре сотрудника Facebook получили престижную премию CAV». Facebook .[ ненадежный источник? ]
  9. ^ ab "Профессор компьютерных наук получил престижную награду". Лондонский университет королевы Марии . 3 февраля 2011 г.
  10. ^ abc Питер О'Херн публикации, проиндексированные Google Scholar
  11. ^ Питер О'Херн в проекте «Генеалогия математики»
  12. ^ ab Рейнольдс, Джон К. (2002). «Логика разделения: логика для общих изменяемы структур данных» (PDF) . LICS .
  13. ^ ab O'Hearn, PW; Pym, DJ (июнь 1999). «Логика сгруппированных импликаций». Bulletin of Symbolic Logic . 5 (2): 215–244. doi :10.2307/421090. JSTOR  421090. S2CID  2948552.
  14. ^ abc "Статический анализатор Infer". fbinfer.com .
  15. ^ "Питер О'Херн". Исследование Facebook .
  16. ^ ab "Питер О'Хирн".
  17. ^ "Питер О'Херн". www0.cs.ucl.ac.uk .
  18. ^ Питер У. О'Хирн, Curriculum Vitae. Архивировано 19 июля 2011 г. в Wayback Machine , Королева Мэри, Лондонский университет , Великобритания.
  19. ^ Хоар, Тони (2003). «Проверяющий компилятор». Журнал ACM . 50 : 63–69. doi :10.1145/602382.602403. S2CID  441648.
  20. ^ О'Херн, Питер; Теннент, Роберт Д. (1997). Языки, подобные Алголу . Кембридж, Массачусетс: Birkhauser Boston. doi :10.1007/978-1-4612-4118-8. ISBN 978-0-8176-3880-1. S2CID  6273486.
  21. ^ «Facebook приобретает активы британского разработчика программного обеспечения для проверки мобильных ошибок Monoidics». TechCrunch . Verizon Media. 18 июля 2013 г.
  22. ^ «Непрерывное рассуждение: масштабирование влияния формальных методов». Исследование Facebook .
  23. ^ "Facebook с открытым исходным кодом RacerD: инструмент, который уже устранил 1000 ошибок в параллельном коде". TechRepublic . 19 октября 2017 г.
  24. ^ "Spring Newsletter". raeng.org.uk . 2012. Архивировано из оригинала 4 сентября 2016 года . Получено 6 июня 2018 года .

Внешние ссылки

 В данной статье используется текст, доступный по лицензии CC BY 4.0.