Питер Уильям O'Hearn FRS FREng [7] [9] (родился 13 июля 1963 в Галифаксе, Новая Шотландия ) является ученым - исследователем в Facebook [15] и профессор из информатики в Университетском колледже Лондона (UCL). [16] Он внес значительный вклад в формальные методы проверки правильности программ. В последние годы эти достижения были использованы при разработке промышленных программных инструментов, которые проводят автоматизированный анализ крупных промышленных кодовых баз. [12]
Образование
О'Хирн получил степень бакалавра информатики в Университете Далхаузи , Галифакс, Новая Шотландия (1985), а затем степени магистра (1987) и доктора философии (1991) в Королевском университете , Кингстон , Онтарио , Канада. Его диссертация была на тему « Семантика невмешательства: естественный подход» под руководством Роберта Д. Теннента. [13] [17]
Карьера и исследования
O'Hearn лучше всего известен логика разделения , [1] теория он разработал с Джоном К. Рейнольдсом , что раскопали новые домены для масштабирования логических рассуждений о коде. Это основано на предыдущих исследованиях О'Хирна и Дэвида Пима по логике для ресурсов, названных сгруппированной логикой . [2] Вместе со Стивеном Бруксом из Университета Карнеги-Меллона О'Хирн создал логику параллельного разделения (CSL), расширив теорию. Тони Хоар , обсуждая грандиозную проблему верификации программ, описал CSL как «решение двух проблем ... согласованности и объектной ориентации». [18] [19]
Вместе со своим бывшим научным руководителем Робертом Д. Теннентом он провел исследование языков программирования, похожих на АЛГОЛ , которое стало книгой « Алголо-подобные языки» . [20]
Логика разделения породила Infer Static Analyzer (Facebook Infer), утилиту статического анализа программ, разработанную командой О'Хирна в Facebook . [3] Проработав более 20 лет в академических кругах, О'Хирн начал работать в Facebook в 2013 году с приобретением Monoidics Ltd, стартапа, который он основал. [21] С момента своего создания Infer позволил инженерам Facebook исправить десятки тысяч ошибок до того, как перейти в производство. [22] Он был открыт в 2016 году и используется Amazon Inc , Spotify , Mozilla , Uber и другими. [3] В 2017 году О'Хирн и его команда открыли исходный код RacerD, автоматизированного инструмента обнаружения статических состояний гонки, который сокращает время, необходимое для выявления потенциальных проблем в параллельном программном обеспечении, как часть платформы Infer. [23]
О'Хирн был доцентом Сиракузского университета , Нью-Йорк , США, с 1990 по 1995 год. Он был читателем по информатике в Лондонском университете королевы Марии с 1996 по 1999 год, а затем до своего переезда был профессором Королевы Марии. в Университетский колледж Лондона . В UCL ему была предоставлена кафедра, спонсируемая Королевской инженерной академией и Microsoft Research . [24] В 1997 году он был приглашенным научным сотрудником в Университете Карнеги-Меллона, а в 2006 году он был приглашенным исследователем в Microsoft Research Cambridge . [17] Сейчас он делит свое время, работая научным сотрудником в Facebook и профессором в UCL. [ необходима цитата ]
Награды и почести
В 2007 году О'Хирн был удостоен награды Королевского общества за заслуги перед исследованием Вольфсона . [7] В 2011 году О'Хирн и Самин Иштиак были удостоены награды «Самая влиятельная газета POPL». [11] Вместе со Стивеном Бруксом из Университета Карнеги-Меллона он был соучредителем премии Гёделя 2016 года за изобретение параллельной логики разделения. [8] Также в 2016 году он был избран членом Королевской инженерной академии (FREng) и получил ежегодную награду CAV (Computer Aided Verification). [9] [10] В 2018 году он был избран членом Королевского общества (FRS), и был удостоен почетным доктором юридических наук из университета Dalhousie . [6] [7] [5] В январе 2019 года О'Хирн был удостоен еще одной награды «Самая влиятельная статья в POPL», которую он разделил с тремя коллегами. [4]
Рекомендации
- ^ a b Рейнольдс, Джон К. (2002). «Логика разделения: логика для общих изменяемых структур данных» (PDF) . LICS .
- ^ а б О'Хирн, PW; Пим, ди-джей (июнь 1999 г.). «Логика сгруппированных следствий» . Вестник символической логики . 5 (2): 215–244. DOI : 10.2307 / 421090 . JSTOR 421090 . S2CID 2948552 .
- ^ а б в «Сделать вывод статического анализатора» . fbinfer.com .
- ^ а б «Премия POPL 2019 за наиболее влиятельную бумагу за исследования, которые привели к выводу Facebook Infer» . Facebook . 17 января 2019.
- ^ a b https://www.dal.ca/news/2018/04/19/introduction-dal-s-honorary-degree-recipients-for-spring-convocat.html
- ^ а б «Выдающиеся ученые, избранные научными сотрудниками и иностранными членами Королевского общества» . royalsociety.org . Проверено 15 мая 2018 .
- ^ а б в г д Анон (2018). "Профессор Питер О'Хирн FRS" . royalsociety.org . Лондон: Королевское общество . Архивировано из оригинала 7 июня 2018 года. Одно или несколько предыдущих предложений включают текст с веб-сайта royalsociety.org, где:
«Весь текст, опубликованный под заголовком« Биография »на страницах профилей участников, доступен по международной лицензии Creative Commons Attribution 4.0 ». - «Архивная копия» . Архивировано 11 ноября 2016 года . Проверено 7 июня 2018 .CS1 maint: заархивированная копия как заголовок ( ссылка ) CS1 maint: bot: исходный статус URL неизвестен ( ссылка )
- ^ а б Чита, Эфи (12–15 июля 2016 г.). «Премия Гёделя 2016 года» . Европейская ассоциация теоретической информатики.
- ^ а б в https://www.raeng.org.uk/about-us/the-fellowship/new-fellows-2016/fellows/peter-o-hearn
- ^ а б О'Салливан, Брайан (5 сентября 2016 г.). «Четыре сотрудника Facebook выиграли престижную награду CAV» . Facebook .
- ^ а б «Профессор информатики получает престижную награду» . Лондонский университет королевы Марии . 3 февраля 2011 г.
- ^ a b c Публикации Питера О'Хирна, проиндексированные Google Scholar
- ^ a b Питер О'Хирн в проекте « Математическая генеалогия»
- ^ Оливье Данви, Питер О'Хирн и Филип Уодлер (редакторы), Festschrift к 70-летию Джона К. Рейнольдса. Теоретическая информатика , 375 (1–3): 1–350, 1 мая 2007 г. От редакции, страницы 1–2. DOI : 10.1016 / j.tcs.2006.12.024
- ^ "Питер О'Хирн" . Facebook Research .
- ^ "Питер О'Хирн" . www0.cs.ucl.ac.uk .
- ^ Б Питер W O'Hearn, Curriculum Vitae архивации 2011-07-19 в Wayback Machine , Queen Mary, Университет Лондона , Великобритания.
- ^ https://www.facebook.com/academics/videos/2228616734102290/?t=3775
- ^ Хоар, Тони (2003). «Проверяющий компилятор» . Журнал ACM . 50 : 63–69. DOI : 10.1145 / 602382.602403 . S2CID 441648 .
- ^ О'Хирн, Питер; Теннент, Роберт Д. (1997). Алголообразные языки . Кембридж, Массачусетс, США: Birkhauser Boston. DOI : 10.1007 / 978-1-4612-4118-8 . ISBN 978-0-8176-3880-1. S2CID 6273486 .
- ^ «Facebook приобретает активы британского разработчика программного обеспечения для проверки мобильных ошибок Monoidics» . TechCrunch . Verizon Media.
- ^ «Непрерывное рассуждение: масштабирование воздействия формальных методов» . Facebook Research .
- ^ «Facebook с открытым исходным кодом RacerD: инструмент, который уже исправил 1000 ошибок в параллельном коде» . TechRepublic . 19 октября 2017.
- ^ «Весенний информационный бюллетень» (PDF) . raeng.org.uk . 2012 г.
Эта статья включает текст, доступный по лицензии CC BY 4.0 .