Peter William O'Hearn FRS FREng [7] [9] (nacido el 13 de julio de 1963 en Halifax, Nueva Escocia ) es un científico investigador en Facebook [15] y profesor de informática en el University College London (UCL). [16] Ha realizado contribuciones significativas a los métodos formales para la corrección del programa. En los últimos años, estos avances se han empleado en el desarrollo de herramientas de software industrial que realizan análisis automatizados de grandes bases de códigos industriales. [12]
Peter O'Hearn FRS FREng | |
---|---|
![]() Peter O'Hearn en el día de admisiones de la Royal Society en Londres, julio de 2018 | |
Nació | Peter William O'Hearn 13 de julio de 1963 Halifax, Nueva Escocia , Canadá |
Nacionalidad | Británico, canadiense |
Ciudadanía | Reino Unido, canadá |
alma mater | Universidad de Dalhousie (BSc) Queen's University (MSc, PhD) |
Conocido por | Lógica de separación [1] Lógica agrupada [2] Analizador estático de inferencia [3] |
Premios |
|
Carrera científica | |
Campos | Lenguajes de programación [12] Análisis de programas Verificación formal Informática teórica [12] |
Instituciones | Facebook University College London Queen Mary University of London Syracuse University |
Tesis | Semántica de la no interferencia: un enfoque natural (1992) |
Asesor de doctorado | Robert D. Tennent [13] |
Influencias | John C. Reynolds [14] |
Sitio web | www0 .cs .ucl .ac .uk / staff / p .ohearn / |
Educación
O'Hearn obtuvo una licenciatura en ciencias de la computación de la Universidad de Dalhousie , Halifax, Nueva Escocia (1985), seguida de una maestría (1987) y un doctorado (1991) de la Universidad de Queen , Kingston , Ontario , Canadá. Su disertación fue sobre Semántica de la no interferencia: un enfoque natural , supervisada por Robert D. Tennent. [13] [17]
Carrera e investigación
O'Hearn es mejor conocido por la lógica de separación , [1] una teoría que desarrolló con John C. Reynolds que descubrió nuevos dominios para escalar el razonamiento lógico sobre el código. Esto se basó en una investigación previa de O'Hearn y David Pym sobre la lógica de los recursos, denominada lógica agrupada . [2] Con Stephen Brookes, de la Carnegie Mellon University , O'Hearn creó Concurrent Separation Logic (CSL), extendiendo la teoría aún más. Tony Hoare , al discutir el gran desafío de la verificación del programa, describió CSL como "resolver dos problemas ... concurrencia y orientación a objetos". [18] [19]
Realizó un estudio de lenguajes de programación que eran similares a ALGOL , con su ex asesor de doctorado Robert D. Tennent, que se convirtió en el libro Algol-Like Languages . [20]
La lógica de separación ha dado lugar al Infer Static Analyzer (Facebook Infer), una utilidad de análisis de programas estáticos desarrollada por el equipo de O'Hearn en Facebook . [3] Después de más de 20 años en el mundo académico, O'Hearn comenzó a trabajar en Facebook en 2013 con la adquisición de Monoidics Ltd, una startup que cofundó. [21] Desde sus inicios, Infer ha permitido a los ingenieros de Facebook resolver decenas de miles de errores antes de llegar a producción. [22] Fue de código abierto en 2016 y es utilizado por Amazon Inc , Spotify , Mozilla , Uber y otros. [3] En 2017, O'Hearn y el equipo crearon RacerD de código abierto, una herramienta automatizada de detección de condición de carrera estática que reduce el tiempo que lleva señalar problemas potenciales en software concurrente, como parte de la plataforma Infer. [23]
O'Hearn fue profesor asistente en la Universidad de Syracuse , Nueva York , Estados Unidos, de 1990 a 1995. Fue lector de ciencias de la computación en la Universidad Queen Mary de Londres de 1996 a 1999 y luego profesor titular en Queen Mary hasta su mudanza. al University College de Londres . En la UCL se le concedió una cátedra patrocinada por la Royal Academy of Engineering y Microsoft Research . [24] En 1997 fue científico invitado en la Universidad Carnegie Mellon y en 2006 fue investigador invitado en Microsoft Research Cambridge . [17] Ahora comparte su tiempo trabajando como científico investigador en Facebook y profesor en UCL. [ cita requerida ]
Premios y honores
En 2007, O'Hearn recibió un premio al mérito de investigación Wolfson de la Royal Society . [7] En 2011, O'Hearn y Samin Ishtiaq recibieron el premio al papel POPL más influyente. [11] Con Stephen Brookes, Carnegie Mellon University , fue co-beneficiario del Premio Gödel 2016 , por la invención de la lógica de separación concurrente. [8] También en 2016, fue elegido miembro de la Real Academia de Ingeniería (FREng) y co-recibió el premio anual CAV (Verificación asistida por computadora). [9] [10] En 2018, fue elegido miembro de la Royal Society (FRS) y recibió un doctorado honorario en derecho de la Universidad de Dalhousie . [6] [7] [5] En enero de 2019, O'Hearn fue honrado con otro premio POPL Paper Award más influyente, que compartió con tres colegas. [4]
Referencias
- ↑ a b Reynolds, John C. (2002). "Lógica de separación: una lógica para estructuras de datos mutables compartidas" (PDF) . LICS .
- ^ a b O'Hearn, PW; Pym, DJ (junio de 1999). "La lógica de las implicaciones agrupadas" . Boletín de Lógica Simbólica . 5 (2): 215–244. doi : 10.2307 / 421090 . JSTOR 421090 . S2CID 2948552 .
- ^ a b c "Inferir analizador estático" . fbinfer.com .
- ^ a b "Premio POPL 2019 Most Influential Paper Award por la investigación que llevó a Facebook Infer" . Facebook . 17 de enero de 2019.
- ^ a b https://www.dal.ca/news/2018/04/19/introducing-dal-s-honorary-degree-recipients-for-spring-convocat.html
- ^ a b "Científicos distinguidos elegidos como becarios y miembros extranjeros de la Royal Society" . royalsociety.org . Consultado el 15 de mayo de 2018 .
- ^ a b c d e Anon (2018). "Profesor Peter O'Hearn FRS" . royalsociety.org . Londres: Royal Society . Archivado desde el original el 7 de junio de 2018. Una o más de las oraciones anteriores incorporan texto del sitio web royalsociety.org donde:
"Todo el texto publicado bajo el título 'Biografía' en las páginas de perfil de los becarios está disponible bajo Creative Commons Attribution 4.0 International License ". - "Copia archivada" . Archivado desde el original el 11 de noviembre de 2016 . Consultado el 7 de junio de 2018 .CS1 maint: copia archivada como título ( enlace ) CS1 maint: bot: estado de URL original desconocido ( enlace )
- ^ a b Chita, Efi (12 a 15 de julio de 2016). "Premio Gödel 2016" . Asociación Europea de Informática Teórica.
- ^ a b c https://www.raeng.org.uk/about-us/the-fellowship/new-fellows-2016/fellows/peter-o-hearn
- ^ a b O'Sullivan, Bryan (5 de septiembre de 2016). "Cuatro empleados de Facebook ganan el prestigioso premio CAV" . Facebook .
- ^ a b "Profesor de Informática gana prestigioso premio" . Universidad Queen Mary de Londres . 3 de febrero de 2011.
- ^ a b c Publicaciones de Peter O'Hearn indexadas por Google Scholar
- ^ a b Peter O'Hearn en el Proyecto de genealogía matemática
- ^ Olivier Danvy, Peter O'Hearn y Philip Wadler (editores), Festschrift para el 70 cumpleaños de John C. Reynolds. Theoretical Computer Science , 375 (1–3): 1–350, 1 de mayo de 2007. Editorial, páginas 1–2. doi : 10.1016 / j.tcs.2006.12.024
- ^ "Peter O'Hearn" . Investigación de Facebook .
- ^ "Peter O'Hearn" . www0.cs.ucl.ac.uk .
- ^ a b Peter W O'Hearn, Curriculum Vitae Archivado el 19 de julio de 2011 en la Wayback Machine , Queen Mary, Universidad de Londres , Reino Unido.
- ^ https://www.facebook.com/academics/videos/2228616734102290/?t=3775
- ^ Hoare, Tony (2003). "El compilador de verificación" . Revista de la ACM . 50 : 63–69. doi : 10.1145 / 602382.602403 . S2CID 441648 .
- ^ O'Hearn, Peter; Tennent, Robert D. (1997). Lenguajes tipo Algol . Cambridge, Massachusetts, Estados Unidos: Birkhauser Boston. doi : 10.1007 / 978-1-4612-4118-8 . ISBN 978-0-8176-3880-1. S2CID 6273486 .
- ^ "Facebook adquiere activos de Monoidics desarrollador de software de comprobación de errores móviles del Reino Unido" . TechCrunch . Verizon Media.
- ^ "Razonamiento continuo: escalar el impacto de los métodos formales" . Investigación de Facebook .
- ^ "Facebook open sources RacerD: una herramienta que ya ha solucionado 1.000 errores en el código concurrente" . TechRepublic . 19 de octubre de 2017.
- ^ "Boletín de primavera" (PDF) . raeng.org.uk . 2012.
Este artículo incorpora texto disponible bajo la licencia CC BY 4.0 .