Питер О'Хирн

Питер О'Хирн
ФРС ФРЕнг
Питер О'Хирн ФРС ФРЕнг
	Питер О'Хирн на в Королевское общество в Лондоне, июль 2018 г. приеме
Рожденный	Питер Уильям О'Хирн ; 13 июля 1963 г. (61 год) ; Галифакс, Новая Шотландия , Канада
Национальность	Британский, Канадский
Гражданство	Великобритания, Канада
Альма-матер	Университет Далхаузи (бакалавр) ; Королевский университет (магистр, доктор философии)
Известный	Логика разделения ; Сгруппированная логика ; Статический анализатор Infer
Награды	Премия IEEE в области кибербезопасности за практику (2021 г.) ; Премия за самую влиятельную бумагу POPL (2019) ; Почетный доктор права Университета Далхаузи (2018). ; Член Королевского общества (FRS) (2018 г.) ; Премия Гёделя (2016). ; Член Королевской инженерной академии (FREng) (2016 г.) ; Премия CAV (компьютерная проверка) (2016 г.) ; Премия за самую влиятельную бумагу POPL (2011) ; Премия Королевского общества Вольфсона за заслуги в области исследований (2007 г.) ;
	Научная карьера
Поля	Языки программирования ; Анализ программы ; Формальная проверка ; Теоретическая информатика
Учреждения	Кружево ; Мета-платформы ; Университетский колледж Лондона ; Лондонский университет королевы Марии ; Сиракузский университет
Диссертация	Семантика невмешательства: естественный подход (1992)
Докторантура	Роберт Д. Теннент
Веб-сайт	www0 .cs .ucl .и .uk /персонал /п .охерн /

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

Образование

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

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

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

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

Логика разделения привела к появлению Infer Static Analyser (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 (компьютерная проверка). ^{[ 7 ]}^{[ 8 ]} В 2018 году он был избран членом Королевского общества (FRS) и удостоен звания почетного доктора права Университета Далхаузи . ^{[ 4 ]}^{[ 5 ]}^{[ 3 ]} В январе 2019 года О'Хирн был удостоен еще одной награды за самую влиятельную работу POPL, которую он разделил с тремя коллегами. ^{[ 2 ]} Институт инженеров по электротехнике и электронике (IEEE) вручил О'Хирну и трем его коллегам из Facebook награду IEEE за практику в области кибербезопасности на своей ежегодной церемонии награждения в октябре 2021 года. ^{[ 1 ]}

Ссылки

^ Jump up to: ^а ^б «Церемония награждения IEEE 2021 — Конференция по безопасному развитию IEEE» .
^ Jump up to: ^а ^б «Награда за самую влиятельную статью POPL 2019 за исследование, которое привело к выводу Facebook» . Фейсбук . 17 января 2019 г.
^ Jump up to: ^а ^б «Представляем почетных кавалеров Даля Весеннего созыва 2018» .
^ Jump up to: ^а ^б «Выдающиеся ученые избраны научными сотрудниками и иностранными членами Королевского общества» . royalsociety.org . Проверено 15 мая 2018 г.
^ Jump up to: ^а ^б ^с ^д ^и Анон (2018). «Профессор Питер О'Хирн, ФРС» . royalsociety.org . Лондон: Королевское общество . Архивировано из оригинала 7 июня 2018 года. Одно или несколько предыдущих предложений включают текст с веб-сайта royalsociety.org, где:
«Весь текст, опубликованный под заголовком «Биография» на страницах профиля стипендиата, доступен по международной лицензии Creative Commons Attribution 4.0 ». -- «Правила, условия и политика | Королевское общество» . Архивировано из оригинала 11 ноября 2016 года . Проверено 7 июня 2018 г. {{cite web}}: CS1 maint: bot: исходный статус URL неизвестен ( ссылка )
^ Jump up to: ^а ^б Чита, Эфи (12–15 июля 2016 г.). «Премия Гёделя 2016» . Европейская ассоциация теоретической информатики.
^ Jump up to: ^а ^б ^с «Стипендиаты Королевской академии 2016» . Архивировано из оригинала 27 марта 2019 года . Проверено 26 мая 2018 г.
^ Jump up to: ^а ^б О'Салливан, Брайан (5 сентября 2016 г.). «Четыре сотрудника Facebook получили престижную награду CAV» . Фейсбук . ^{[ ненадежный источник? ]}
^ Jump up to: ^а ^б «Профессор информатики получил престижную награду» . Лондонский университет королевы Марии . 3 февраля 2011 г.
^ Jump up to: ^а ^б ^с Публикации Питера О'Хирна, проиндексированные Google Scholar
^ Jump up to: ^а ^б Питер О'Хирн в проекте «Математическая генеалогия»
^ Jump up to: ^а ^б Рейнольдс, Джон К. (2002). «Логика разделения: логика для общих изменяемых структур данных» (PDF) . ЛИКС .
^ Jump up to: ^а ^б О'Хирн, PW; Пим, диджей (июнь 1999 г.). «Логика объединенных импликаций». Бюллетень символической логики . 5 (2): 215–244. дои : 10.2307/421090 . JSTOR 421090 . S2CID 2948552 .
^ Jump up to: ^а ^б ^с «Вывод статического анализатора» . fbinfer.com .
^ «Питер О'Хирн» . Исследование Фейсбука .
^ Jump up to: ^а ^б «Питер О'Хирн» .
^ «Питер О'Хирн» . www0.cs.ucl.ac.uk.
^ Jump up to: ^а ^б Питер В. О'Хирн, Биографическая справка. Архивировано 19 июля 2011 года в Wayback Machine , Королева Мария, Лондонский университет , Великобритания.
^ Хоар, Тони (2003). «Проверочный компилятор» . Журнал АКМ . 50 : 63–69. дои : 10.1145/602382.602403 . S2CID 441648 .
^ О'Хирн, Питер; Теннент, Роберт Д. (1997). Алголоподобные языки . Кембридж, Массачусетс: Биркхаузер Бостон. дои : 10.1007/978-1-4612-4118-8 . ISBN 978-0-8176-3880-1 . S2CID 6273486 .
^ «Facebook приобретает активы британского разработчика программного обеспечения для проверки мобильных ошибок Monoidics» . ТехКранч . Веризон Медиа. 18 июля 2013 г.
^ «Непрерывное рассуждение: масштабирование влияния формальных методов» . Исследование Фейсбука .
^ «Facebook с открытым исходным кодом RacerD: инструмент, который уже устранил 1000 ошибок в параллельном коде» . Техреспублика . 19 октября 2017 г.
^ «Весенний вестник» . raeng.org.uk . 2012. Архивировано из оригинала 4 сентября 2016 года . Проверено 6 июня 2018 г.

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

СМИ, связанные с Питером О'Хирном, на Викискладе?

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

[secdev.ieee.org-1] Jump up to: ^а ^б «Церемония награждения IEEE 2021 — Конференция по безопасному развитию IEEE» .

[poplaward2-2] Jump up to: ^а ^б «Награда за самую влиятельную статью POPL 2019 за исследование, которое привело к выводу Facebook» . Фейсбук . 17 января 2019 г.

[dal.ca-3] Jump up to: ^а ^б «Представляем почетных кавалеров Даля Весеннего созыва 2018» .

[royalsociety.org-4] Jump up to: ^а ^б «Выдающиеся ученые избраны научными сотрудниками и иностранными членами Королевского общества» . royalsociety.org . Проверено 15 мая 2018 г.

[frs-5] Jump up to: ^а ^б ^с ^д ^и Анон (2018). «Профессор Питер О'Хирн, ФРС» . royalsociety.org . Лондон: Королевское общество . Архивировано из оригинала 7 июня 2018 года. Одно или несколько предыдущих предложений включают текст с веб-сайта royalsociety.org, где:
«Весь текст, опубликованный под заголовком «Биография» на страницах профиля стипендиата, доступен по международной лицензии Creative Commons Attribution 4.0 ». -- «Правила, условия и политика | Королевское общество» . Архивировано из оригинала 11 ноября 2016 года . Проверено 7 июня 2018 г. {{cite web}}: CS1 maint: bot: исходный статус URL неизвестен ( ссылка )

[auto-6] Jump up to: ^а ^б Чита, Эфи (12–15 июля 2016 г.). «Премия Гёделя 2016» . Европейская ассоциация теоретической информатики.

[raeng.org.uk-7] Jump up to: ^а ^б ^с «Стипендиаты Королевской академии 2016» . Архивировано из оригинала 27 марта 2019 года . Проверено 26 мая 2018 г.

[fbcav-8] Jump up to: ^а ^б О'Салливан, Брайан (5 сентября 2016 г.). «Четыре сотрудника Facebook получили престижную награду CAV» . Фейсбук . ^{[ ненадежный источник? ]}

[poplaward-9] Jump up to: ^а ^б «Профессор информатики получил престижную награду» . Лондонский университет королевы Марии . 3 февраля 2011 г.

[gs-10] Jump up to: ^а ^б ^с Публикации Питера О'Хирна, проиндексированные Google Scholar

[mathgene-11] Jump up to: ^а ^б Питер О'Хирн в проекте «Математическая генеалогия»

[lics02-12] Jump up to: ^а ^б Рейнольдс, Джон К. (2002). «Логика разделения: логика для общих изменяемых структур данных» (PDF) . ЛИКС .

[bi-13] Jump up to: ^а ^б О'Хирн, PW; Пим, диджей (июнь 1999 г.). «Логика объединенных импликаций». Бюллетень символической логики . 5 (2): 215–244. дои : 10.2307/421090 . JSTOR 421090 . S2CID 2948552 .

[fbinfer-14] Jump up to: ^а ^б ^с «Вывод статического анализатора» . fbinfer.com .

[15] «Питер О'Хирн» . Исследование Фейсбука .

[www0.cs.ucl.ac.uk-16] Jump up to: ^а ^б «Питер О'Хирн» .

[17] «Питер О'Хирн» . www0.cs.ucl.ac.uk.

[cv-18] Jump up to: ^а ^б Питер В. О'Хирн, Биографическая справка. Архивировано 19 июля 2011 года в Wayback Machine , Королева Мария, Лондонский университет , Великобритания.

[19] Хоар, Тони (2003). «Проверочный компилятор» . Журнал АКМ . 50 : 63–69. дои : 10.1145/602382.602403 . S2CID 441648 .

[20] О'Хирн, Питер; Теннент, Роберт Д. (1997). Алголоподобные языки . Кембридж, Массачусетс: Биркхаузер Бостон. дои : 10.1007/978-1-4612-4118-8 . ISBN 978-0-8176-3880-1 . S2CID 6273486 .

[21] «Facebook приобретает активы британского разработчика программного обеспечения для проверки мобильных ошибок Monoidics» . ТехКранч . Веризон Медиа. 18 июля 2013 г.

[22] «Непрерывное рассуждение: масштабирование влияния формальных методов» . Исследование Фейсбука .

[23] «Facebook с открытым исходным кодом RacerD: инструмент, который уже устранил 1000 ошибок в параллельном коде» . Техреспублика . 19 октября 2017 г.

[24] «Весенний вестник» . raeng.org.uk . 2012. Архивировано из оригинала 4 сентября 2016 года . Проверено 6 июня 2018 г.

[ 12 ]

[ 13 ]

[ 14 ]

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]

[ 8 ]

[ 9 ]

[ 10 ]

[ 11 ]

[ 15 ]

[ 16 ]

[ 17 ]

[ 18 ]

[ 19 ]

[ 20 ]

[ 21 ]

[ 22 ]

[ 23 ]

[ 24 ]

v т и Члены Королевского общества, избранные в 2018 году
Товарищи	Джим Аль-Халили Полли Арнольд Джиллиан Бэнфилд Маргарет Бримбл Нил Брокдорф Фрэнк Карузо Винченцо Серундоло Кевин Костелло Роберт Крэбтри Филип Дэвид Питер Даян Ричард Диксон Грегори Эджкомб Вэньфэй Фан Роджер Гуди Робин Граймс Грегори Хэннон Демис Хассабис Джуди Херст Грэм Джеймсон Харрен Джоти Софиен Камун Эндрю Кинг Дмитрий Куллманн Доминик Квятковски Ришар Марэ Кэти Мартин Илон Маск Питер О'Хирн Василис Пахнис Трейси Палмер Колин Прентис Лалита Рамакришнан Нэнси Рид Грэм Ричардс Дэвид Ричардсон Шейла Роуэн Ингрид Шеффер Мишель Симмонс John Smol Тимоти Софтли Джон Спикман Грэм Стивенс Анжела Клиент Чарльз Суонтон Питер Вишер Гай Уилкинсон Джорди Уильямсон Дэниел Уайз Nikolay Zheludev
Почетный	Дэвид Уиллеттс (барон Уиллетс из Хаванта)
Иностранный	Кэролайн Бертоцци Мартин Чалфи Себсебе Демисью Джеффри Фридман Фабиола Джанотти Альбрехт Хофманн Батлер Лэмпсон Туллио Поццан Йоахим Зауэр Ади Шамир

Базы данных авторитетного контроля
Международный	ЯВЛЯЮТСЯ ВИАФ WorldCat
Национальный	Франция Данные БнФ Германия Соединенные Штаты Нидерланды
академики	Ассоциация вычислительной техники ДБЛП Google Академика MathSciNet Проект математической генеалогии ОРЦИД
Другой	ИдРеф