J u m p t o c o n t e n t
M a i n m e n u
M a i n m e n u
N a v i g a t i o n
● M a i n p a g e ● C o n t e n t s ● C u r r e n t e v e n t s ● R a n d o m a r t i c l e ● A b o u t W i k i p e d i a ● C o n t a c t u s ● D o n a t e
C o n t r i b u t e
● H e l p ● L e a r n t o e d i t ● C o m m u n i t y p o r t a l ● R e c e n t c h a n g e s ● U p l o a d f i l e
S e a r c h
Search
A p p e a r a n c e
● C r e a t e a c c o u n t ● L o g i n
P e r s o n a l t o o l s
● C r e a t e a c c o u n t ● L o g i n
P a g e s f o r l o g g e d o u t e d i t o r s l e a r n m o r e ● C o n t r i b u t i o n s ● T a l k
( T o p )
1 E d u c a t i o n
2 C a r e e r a n d r e s e a r c h
T o g g l e C a r e e r a n d r e s e a r c h s u b s e c t i o n
2 . 1 A w a r d s a n d h o n o u r s
3 R e f e r e n c e s
4 E x t e r n a l l i n k s
T o g g l e t h e t a b l e o f c o n t e n t s
P e t e r O ' H e a r n
4 l a n g u a g e s
● ت ۆ ر ک ج ه ● D e u t s c h ● ف ا ر س ی ● F r a n ç a i s
E d i t l i n k s
● A r t i c l e ● T a l k
E n g l i s h
● R e a d ● E d i t ● V i e w h i s t o r y
T o o l s
T o o l s
A c t i o n s
● R e a d ● E d i t ● V i e w h i s t o r y
G e n e r a l
● W h a t l i n k s h e r e ● R e l a t e d c h a n g e s ● U p l o a d f i l e ● S p e c i a l p a g e s ● P e r m a n e n t l i n k ● P a g e i n f o r m a t i o n ● C i t e t h i s p a g e ● G e t s h o r t e n e d U R L ● D o w n l o a d Q R c o d e ● W i k i d a t a i t e m
P r i n t / e x p o r t
● D o w n l o a d a s P D F ● P r i n t a b l e v e r s i o n
A p p e a r a n c e
F r o m W i k i p e d i a , t h e f r e e e n c y c l o p e d i a
Research scientist (born 1963)
Peter William O'Hearn FRS FREng [5] [7] Halifax, Nova Scotia ), formerly a research scientist at Meta ,[15] [16] Professor of Computer science at University College London (UCL).[17] formal methods for program correctness. In recent years these advances have been employed in developing industrial software tools that conduct automated analysis of large industrial codebases.[10]
Education
[ edit ]
O'Hearn attained a BSc degree in computer science from Dalhousie University , Halifax, Nova Scotia (1985), followed by MSc (1987) and PhD (1991) degrees from Queen's University , Kingston , Ontario , Canada. His dissertation was on Semantics of Non-interference: A natural approach , supervised by Robert D. Tennent.[11] [18]
Career and research
[ edit ]
O'Hearn is best known for separation logic ,[12] John C. Reynolds that unearthed new domains for scaling logical reasoning about code. This built on prior research from O'Hearn and David Pym on logic for resources, termed bunched logic .[13] Carnegie Mellon University , O'Hearn created Concurrent Separation Logic (CSL), extending the theory further. Tony Hoare , in discussing the grand challenge of program verification, described CSL as "solving two problems...concurrecy and object orientation".[19]
He conducted a study of programming languages which were similar to ALGOL , with his former doctoral advisor Robert D. Tennent, which became the book Algol-Like Languages .[20]
Separation logic has given rise to the Infer Static Analyzer (Facebook Infer), a static program analysis utility developed by O'Hearn's team at Facebook .[14] [21] [22] Amazon Inc , Spotify , Mozilla , Uber , and others.[14] [23]
O'Hearn was an assistant professor at Syracuse University , New York , United States, from 1990 to 1995.
He was a reader in computer science at Queen Mary University of London from 1996 to 1999 and then a full professor at Queen Mary until his move to University College London . At UCL he was granted a chair sponsored by the Royal Academy of Engineering and Microsoft Research .[24] Carnegie Mellon University and in 2006 he was a visiting researcher at Microsoft Research Cambridge .[18] [16]
Awards and honours
[ edit ]
In 2007, O'Hearn was granted a Royal Society Wolfson Research Merit Award .[5] [9] Carnegie Mellon University , he was co-recipient of the 2016 Gödel Prize , for the invention of Concurrent Separation Logic.[6] Fellow of the Royal Academy of Engineering (FREng) and co-received the annual CAV (Computer Aided Verification) award.[7] [8] Fellow of the Royal Society (FRS), and was bestowed with an Honorary Doctor of Laws from Dalhousie University .[4] [5] [3] [2] Institute of Electrical and Electronics Engineers (IEEE) granted O'Hearn and three of his Facebook colleagues an IEEE Cybersecurity Award for Practice at their annual awards ceremony in October, 2021.[1]
References
[ edit ]
^ a b "Introducing Dal's honorary degree recipients for Spring Convocation 2018" .
^ a b "Distinguished scientists elected as Fellows and Foreign Members of the Royal Society" . royalsociety.org . Retrieved 15 May 2018 .
^ a b c d e Anon (2018). "Professor Peter O'Hearn FRS" . royalsociety.org . London: Royal Society . Archived from the original on 7 June 2018.
“All text published under the heading 'Biography' on Fellow profile pages is available under Creative Commons Attribution 4.0 International License .” --"Terms, conditions and policies | Royal Society" . Archived from the original on 11 November 2016. Retrieved 7 June 2018 .{{cite web }}: CS1 maint: bot: original URL status unknown (link )
^ a b Chita, Efi (12–15 July 2016). "2016 Gödel Prize" . European Association for Theoretical Computer Science.
^ a b c "Royal Academy Fellows 2016" . Archived from the original on 27 March 2019. Retrieved 26 May 2018 .
^ a b O'Sullivan, Bryan (5 September 2016). "Four Facebook Employees Win the Prestigious CAV Award" . Facebook . [unreliable source?
^ a b "Computer Science professor wins prestigious award" . Queen Mary University of London . 3 February 2011.
^ a b c Peter O'Hearn publications indexed by Google Scholar
^ a b Peter O'Hearn at the Mathematics Genealogy Project
^ a b Reynolds, John C. (2002). "Separation Logic: A Logic for Shared Mutable Data Structures" (PDF) . LICS .
^ a b O'Hearn, P. W.; Pym, D. J. (June 1999). "The Logic of Bunched Implications". Bulletin of Symbolic Logic 5 2 ): 215–244. doi :10.2307/421090 . JSTOR 421090 . S2CID 2948552 .
^ a b c "Infer static analyzer" . fbinfer.com .
^ "Peter O'Hearn" . Facebook Research .
^ a b "Peter O'Hearn" .
^ "Peter O'Hearn" . www0.cs.ucl.ac.uk .
^ a b Peter W O'Hearn, Curriculum Vitae Archived 19 July 2011 at the Wayback Machine , Queen Mary, University of London , UK.
^ Hoare, Tony (2003). "The verifying compiler" . Journal of the ACM . 50 doi :10.1145/602382.602403 . S2CID 441648 .
^ O'Hearn, Peter; Tennent, Robert D. (1997). Algol-Like Languages . Cambridge, MA: Birkhauser Boston. doi :10.1007/978-1-4612-4118-8 . ISBN 978-0-8176-3880-1 S2CID 6273486 .
^ "Facebook Acquires Assets Of UK Mobile Bug-Checking Software Developer Monoidics" . TechCrunch . Verizon Media. 18 July 2013.
^ "Continuous Reasoning: Scaling the Impact of Formal Methods" . Facebook Research .
^ "Facebook open sources RacerD: A tool that's already squashed 1,000 bugs in concurrent code" . TechRepublic . 19 October 2017.
^ "Spring Newsletter" . raeng.org.uk . 2012. Archived from the original on 4 September 2016. Retrieved 6 June 2018 .
External links
[ edit ]
text available under the CC BY 4.0 license.
t
e
Fellows
Honorary
Foreign
International
National
Academics
Other
R e t r i e v e d f r o m " https://en.wikipedia.org/w/index.php?title=Peter_O%27Hearn&oldid=1206447603 " C a t e g o r i e s : ● 1 9 6 3 b i r t h s ● L i v i n g p e o p l e ● P e o p l e f r o m H a l i f a x , N o v a S c o t i a ● D a l h o u s i e U n i v e r s i t y a l u m n i ● Q u e e n ' s U n i v e r s i t y a t K i n g s t o n a l u m n i ● C a n a d i a n e m i g r a n t s t o E n g l a n d ● B r i t i s h c o m p u t e r s c i e n t i s t s ● C a n a d i a n c o m p u t e r s c i e n t i s t s ● F o r m a l m e t h o d s p e o p l e ● C a n a d i a n F e l l o w s o f t h e R o y a l S o c i e t y ● F e l l o w s o f t h e R o y a l A c a d e m y o f E n g i n e e r i n g ● S y r a c u s e U n i v e r s i t y f a c u l t y ● A c a d e m i c s o f Q u e e n M a r y U n i v e r s i t y o f L o n d o n ● A c a d e m i c s o f U n i v e r s i t y C o l l e g e L o n d o n ● F a c e b o o k e m p l o y e e s ● G ö d e l P r i z e l a u r e a t e s ● R o y a l S o c i e t y W o l f s o n R e s e a r c h M e r i t A w a r d h o l d e r s H i d d e n c a t e g o r i e s : ● C S 1 m a i n t : b o t : o r i g i n a l U R L s t a t u s u n k n o w n ● A l l a r t i c l e s l a c k i n g r e l i a b l e r e f e r e n c e s ● A r t i c l e s l a c k i n g r e l i a b l e r e f e r e n c e s f r o m N o v e m b e r 2 0 2 2 ● W e b a r c h i v e t e m p l a t e w a y b a c k l i n k s ● A r t i c l e s w i t h s h o r t d e s c r i p t i o n ● S h o r t d e s c r i p t i o n i s d i f f e r e n t f r o m W i k i d a t a ● U s e C a n a d i a n E n g l i s h f r o m A p r i l 2 0 1 8 ● A l l W i k i p e d i a a r t i c l e s w r i t t e n i n C a n a d i a n E n g l i s h ● U s e d m y d a t e s f r o m A p r i l 2 0 1 8 ● A r t i c l e s w i t h h C a r d s ● C o m m o n s l i n k i s t h e p a g e n a m e ● A r t i c l e s w i t h i m p o r t e d C r e a t i v e C o m m o n s A t t r i b u t i o n 4 . 0 t e x t ● A r t i c l e s w i t h I S N I i d e n t i f i e r s ● A r t i c l e s w i t h V I A F i d e n t i f i e r s ● A r t i c l e s w i t h W o r l d C a t E n t i t i e s i d e n t i f i e r s ● A r t i c l e s w i t h B N F i d e n t i f i e r s ● A r t i c l e s w i t h B N F d a t a i d e n t i f i e r s ● A r t i c l e s w i t h G N D i d e n t i f i e r s ● A r t i c l e s w i t h L C C N i d e n t i f i e r s ● A r t i c l e s w i t h N T A i d e n t i f i e r s ● A r t i c l e s w i t h A C M - D L i d e n t i f i e r s ● A r t i c l e s w i t h D B L P i d e n t i f i e r s ● A r t i c l e s w i t h G o o g l e S c h o l a r i d e n t i f i e r s ● A r t i c l e s w i t h M A T H S N i d e n t i f i e r s ● A r t i c l e s w i t h M G P i d e n t i f i e r s ● A r t i c l e s w i t h O R C I D i d e n t i f i e r s ● A r t i c l e s w i t h S U D O C i d e n t i f i e r s
● T h i s p a g e w a s l a s t e d i t e d o n 1 2 F e b r u a r y 2 0 2 4 , a t 0 5 : 1 1 ( U T C ) . ● T e x t i s a v a i l a b l e u n d e r t h e C r e a t i v e C o m m o n s A t t r i b u t i o n - S h a r e A l i k e L i c e n s e 4 . 0 ;
a d d i t i o n a l t e r m s m a y a p p l y . B y u s i n g t h i s s i t e , y o u a g r e e t o t h e T e r m s o f U s e a n d P r i v a c y P o l i c y . W i k i p e d i a ® i s a r e g i s t e r e d t r a d e m a r k o f t h e W i k i m e d i a F o u n d a t i o n , I n c . , a n o n - p r o f i t o r g a n i z a t i o n . ● P r i v a c y p o l i c y ● A b o u t W i k i p e d i a ● D i s c l a i m e r s ● C o n t a c t W i k i p e d i a ● C o d e o f C o n d u c t ● D e v e l o p e r s ● S t a t i s t i c s ● C o o k i e s t a t e m e n t ● M o b i l e v i e w
Media related to Peter O'Hearn at Wikimedia Commons
This article incorporates text available under the CC BY 4.0 license.
