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 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,634 people in its urban area. The ...

), formerly a research scientist at

Meta Meta (from the Greek μετά, '' meta'', meaning "after" or "beyond") is a prefix meaning "more comprehensive" or "transcending". In modern nomenclature, ''meta''- can also serve as a prefix meaning self-referential, as a field of study or ende ...

, is a Distinguished Engineer at Lacework and a

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

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 Applied science, practical discipli ...

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 expec ...

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 Dalhousie University (commonly known as Dal) is a large public research university in Nova Scotia Nova Scotia ( ; ; ) is one of the thirteen provinces and territories of Canada. It is one of the three Maritime provinces and one of the fou ...

, 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 Ca ...

, 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 In computer science, separation logic is an extension of Hoare logic, a way of reasoning about programs. It was developed by John C. Reynolds, Peter O'Hearn, Samin Ishtiaq and Hongseok Yang, drawing upon early work by Rod Burstall. The assertion l ...

, 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 Carnegie Mellon University (CMU) is a private research university in Pittsburgh, Pennsylvania. One of its predecessors was established in 1900 by Andrew Carnegie as the Carnegie Technical Schools; it became the Carnegie Institute of Technology ...

, 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 c ...

, 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 Infer, sometimes referred to as "Facebook Infer", is a static code analysis tool developed by an engineering team at Facebook along with open-source contributors. It provides support for Java, C, C++, and Objective-C, and is deployed at Facebook ...

(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 i ...

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 M ...

. 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, wi ...

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), package ...

, 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 Syracuse University (informally 'Cuse or SU) is a Private university, private research university in Syracuse, New York. Established in 1870 with roots in the Methodist Episcopal Church, the university has been nonsectarian since 1920. Locate ...

New York New York most commonly refers to: * New York City, the most populous city in the United States, located in the state of New York * New York (state), a state in the northeastern United States New York may also refer to: Film and television * '' ...

, 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 The Royal Academy of Engineering (RAEng) is the United Kingdom's national academy of engineering. The Academy was founded in June 1976 as the Fellowship of Engineering with support from Prince Philip, Duke of Edinburgh, who became the first senior ...

and

Microsoft Research 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 ...

. In 1997 he was a visiting scientist at

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,

, 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 Inter ...

, 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 science, natural knowledge, incl ...

(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 (LL. ...

from

. 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