Peter William O'Hearn One or more of the preceding sentences incorporates text from the royalsociety.org website where: (born 13 July 1963 in

Halifax, Nova Scotia Halifax is the capital and largest municipality of the Provinces and territories of Canada, Canadian province of Nova Scotia, and the largest municipality in Atlantic Canada. As of the 2021 Census, the municipal population was 439,819, with 348 ...

), formerly a research scientist at Meta, is a Distinguished Engineer at Lacework and a

Professor Professor (commonly abbreviated as Prof.) is an academic rank at universities and other post-secondary education and research institutions in most countries. Literally, ''professor'' derives from Latin as a "person who professes". Professors ...

Computer science Computer science is the study of computation, automation, and information. Computer science spans theoretical disciplines (such as algorithms, theory of computation, information theory, and automation) to practical disciplines (includi ...

University College London , mottoeng = Let all come who by merit deserve the most reward , established = , type = Public research university , endowment = £143 million (2020) , budget = ...

(UCL). He has made significant contributions to

formal methods In computer science, formal methods are mathematically rigorous techniques for the specification, development, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the exp ...

for program correctness. In recent years these advances have been employed in developing industrial software tools that conduct automated analysis of large industrial codebases.

Education

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 Ontario ( ; ) is one of the thirteen provinces and territories of Canada.Ontario is located in the geographic eastern half of Canada, but it has historically and politically been considered to be part of Central Canada. Located in Central C ...

, Canada. His dissertation was on ''Semantics of Non-interference: A natural approach'', supervised by Robert D. Tennent.Peter W O'Hearn, Curriculum Vitae
,

Queen Mary, University of London , mottoeng = With united powers , established = 1785 – The London Hospital Medical College1843 – St Bartholomew's Hospital Medical College1882 – Westfield College1887 – East London College/Queen Mary College , type = Public researc ...

, UK.

Career and research

O'Hearn is best known for separation logic, a theory he developed with

John C. Reynolds John Charles Reynolds (June 1, 1935 – April 28, 2013) was an American computer scientist. Education and affiliations John Reynolds studied at Purdue University and then earned a Doctor of Philosophy (Ph.D.) in theoretical physics from Harvard U ...

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. With Stephen Brookes, Carnegie Mellon University, O'Hearn created Concurrent Separation Logic (CSL), extending the theory further.

Tony Hoare Sir Charles Antony Richard Hoare (Tony Hoare or C. A. R. Hoare) (born 11 January 1934) is a British computer scientist who has made foundational contributions to programming languages, algorithms, operating systems, formal verification, and ...

, in discussing the grand challenge of program verification, described CSL as "solving two problems...concurrecy and object orientation". He conducted a study of programming languages which were similar to

ALGOL ALGOL (; short for "Algorithmic Language") is a family of imperative computer programming languages originally developed in 1958. ALGOL heavily influenced many other languages and was the standard method for algorithm description used by the ...

, with his former doctoral advisor Robert D. Tennent, which became the book ''Algol-Like Languages''. Separation logic has given rise to the Infer Static Analyzer (Facebook Infer), a

static program analysis In computer science, static program analysis (or static analysis) is the analysis of computer programs performed without executing them, in contrast with dynamic program analysis, which is performed on programs during their execution. The term ...

utility developed by O'Hearn's team at

Facebook Facebook is an online social media and social networking service owned by American company Meta Platforms. Founded in 2004 by Mark Zuckerberg with fellow Harvard College students and roommates Eduardo Saverin, Andrew McCollum, Dustin Mosk ...

. After 20 plus years in academia, O'Hearn began working at Facebook in 2013 with the acquisition of Monoidics Ltd, a startup he cofounded. Since its inception, Infer has enabled Facebook engineers to resolve tens of thousands of bugs before reaching production. It was open sourced in 2016, and is used by

Amazon Inc Amazon.com, Inc. ( ) is an American multinational technology company focusing on e-commerce, cloud computing, online advertising, digital streaming, and artificial intelligence. It has been referred to as "one of the most influential economi ...

Spotify Spotify (; ) is a proprietary Swedish audio streaming and media services provider founded on 23 April 2006 by Daniel Ek and Martin Lorentzon. It is one of the largest music streaming service providers, with over 456 million monthly active us ...

Mozilla Mozilla (stylized as moz://a) is a free software community founded in 1998 by members of Netscape. The Mozilla community uses, develops, spreads and supports Mozilla products, thereby promoting exclusively free software and open standards, w ...

Uber Uber Technologies, Inc. (Uber), based in San Francisco, provides mobility as a service, ride-hailing (allowing users to book a car and driver to transport them in a way similar to a taxi), food delivery (Uber Eats and Postmates), packa ...

, and others. In 2017, O'Hearn and the team open sourced RacerD, an automated static race condition detection tool that reduces the time it takes to flag potential problems in concurrent software, as part of the Infer platform. O'Hearn was an assistant professor at Syracuse University, New York, United States, from 1990 to 1995. He was a

reader A reader is a person who reads. It may also refer to: Computing and technology * Adobe Reader (now Adobe Acrobat), a PDF reader * Bible Reader for Palm, a discontinued PDA application * A card reader, for extracting data from various forms of ...

in computer science at

Queen Mary University of London , mottoeng = With united powers , established = 1785 – The London Hospital Medical College1843 – St Bartholomew's Hospital Medical College1882 – Westfield College1887 – East London College/Queen Mary College , type = Public researc ...

from 1996 to 1999 and then a full professor at Queen Mary until his move to

University College London , mottoeng = Let all come who by merit deserve the most reward , established = , type = Public research university , endowment = £143 million (2020) , budget = ...

. At UCL he was granted a Chair sponsored by the Royal Academy of Engineering and Microsoft Research. In 1997 he was a visiting scientist at Carnegie Mellon University and in 2006 he was a visiting researcher at

Microsoft Research Cambridge Microsoft Research (MSR) is the research subsidiary of Microsoft. It was created in 1991 by Richard Rashid, Bill Gates and Nathan Myhrvold with the intent to advance state-of-the-art computing and solve difficult world problems through technologi ...

. He now shares his time working as a Distinguished Engineer at Lacework and a professor at UCL.

Awards and honours

In 2007, O'Hearn was granted a

Royal Society Wolfson Research Merit Award The Royal Society Wolfson Research Merit Award was an award made by the Royal Society from 2000 to 2020. It was administered by the Royal Society and jointly funded by the Wolfson Foundation and the UK Office of Science and Technology, to provide ...

. In 2011, O'Hearn and Samin Ishtiaq were awarded a Most Influential POPL Paper Award. With Stephen Brookes, Carnegie Mellon University, he was co-recipient of the 2016

Gödel Prize The Gödel Prize is an annual prize for outstanding papers in the area of theoretical computer science, given jointly by the European Association for Theoretical Computer Science (EATCS) and the Association for Computing Machinery Special Interes ...

, for the invention of Concurrent Separation Logic. Also in 2016, he was elected

Fellow of the Royal Academy of Engineering Fellowship of the Royal Academy of Engineering (FREng) is an award and fellowship for engineers who are recognised by the Royal Academy of Engineering as being the best and brightest engineers, inventors and technologists in the UK and from aroun ...

(FREng) and co-received the annual CAV (Computer Aided Verification) award. In 2018, he was elected

Fellow of the Royal Society Fellowship of the Royal Society (FRS, ForMemRS and HonFRS) is an award granted by the judges of the Royal Society of London to individuals who have made a "substantial contribution to the improvement of natural knowledge, including mathemat ...

(FRS), and was bestowed with an Honorary

Doctor of Laws A Doctor of Law is a degree in law. The application of the term varies from country to country and includes degrees such as the Doctor of Juridical Science (J.S.D. or S.J.D), Juris Doctor (J.D.), Doctor of Philosophy (Ph.D.), and Legum Doctor ...

from Dalhousie University. January 2019 saw O'Hearn honoured with another Most Influential POPL Paper Award, which he shared with three colleagues. The 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.

References

External links

* {{DEFAULTSORT:Ohearn, Peter 1963 births Living people People from Halifax, Nova Scotia Dalhousie University alumni Queen's University at Kingston alumni Canadian emigrants to England British computer scientists Canadian computer scientists Formal methods people Canadian Fellows of the Royal Society Fellows of the Royal Academy of Engineering Syracuse University faculty Academics of Queen Mary University of London Academics of University College London Facebook employees Gödel Prize laureates Royal Society Wolfson Research Merit Award holders