Peter William O'Hearn (born 13 July 1963 in

Halifax, Nova Scotia Halifax is the capital and most populous municipality of the Provinces and territories of Canada, Canadian province of Nova Scotia, and the most populous municipality in Atlantic Canada. As of 2024, it is estimated that the population of the H ...

), is a researcher a
Meta AI (FAIR)
and a

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

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

University College London University College London (Trade name, branded as UCL) is a Public university, public research university in London, England. It is a Member institutions of the University of London, member institution of the Federal university, federal Uni ...

(UCL). He has made significant contributions to

formal methods In computer science, formal methods are mathematics, mathematically rigorous techniques for the formal specification, specification, development, Program analysis, analysis, and formal verification, verification of software and computer hardware, ...

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, Canada, with three campuses in Halifax, Nova Scotia, Halifax, a fourth in Bible Hill, Nova Scotia, Bible Hill, and a second medical school campus ...

, Halifax, Nova Scotia (1985), followed by MSc (1987) and PhD (1991) degrees from Queen's University,

Kingston Kingston may refer to: Places * List of places called Kingston, including the six most populated: ** Kingston, Jamaica ** Kingston upon Hull, England ** City of Kingston, Victoria, Australia ** Kingston, Ontario, Canada ** Kingston upon Thames, ...

Ontario Ontario is the southernmost Provinces and territories of Canada, province of Canada. Located in Central Canada, Ontario is the Population of Canada by province and territory, country's most populous province. As of the 2021 Canadian census, it ...

, 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 Queen Mary University of London (QMUL, or informally QM, and formerly Queen Mary and Westfield College) is a public research university in Mile End, East London, England. It is a member institution of the federal University of London. Today, ...

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

, 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, United States. The institution was established in 1900 by Andrew Carnegie as the Carnegie Technical Schools. In 1912, it became the Carnegie Institu ...

, O'Hearn created Concurrent Separation Logic (CSL), extending the theory further.

Tony Hoare Sir Charles Antony Richard Hoare (; born 11 January 1934), also known as C. A. R. Hoare, 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 (also known as static analysis or static simulation) is the analysis of computer programs performed without executing them, in contrast with dynamic program analysis, which is performed on programs duri ...

utility developed by O'Hearn's team at

Facebook Facebook is a social media and social networking service owned by the American technology conglomerate Meta Platforms, Meta. Created in 2004 by Mark Zuckerberg with four other Harvard College students and roommates, Eduardo Saverin, Andre ...

. 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., doing business as Amazon, is an American Multinational corporation, multinational technology company engaged in e-commerce, cloud computing, online advertising, digital streaming, and artificial intelligence. Founded in 1994 ...

Spotify Spotify (; ) is a List of companies of Sweden, Swedish Music streaming service, audio streaming and media service provider founded on 23 April 2006 by Daniel Ek and Martin Lorentzon. , it is one of the largest providers of music streaming services ...

Mozilla Mozilla is a free software community founded in 1998 by members of Netscape. The Mozilla community uses, develops, publishes and supports Mozilla products, thereby promoting free software and open standards. The community is supported institution ...

Uber Uber Technologies, Inc. is an American multinational transportation company that provides Ridesharing company, ride-hailing services, courier services, food delivery, and freight transport. It is headquartered in San Francisco, California, a ...

, 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. From 2021-2024 Peter led the development of a Code Security product for the Cybersecurity company Lacework. He returned to Meta to join the AI team in the Fall of 2024. 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, United States. It was established in 1870 with roots in the Methodist Episcopal Church but has been nonsectarian since 1920 ...

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

, United States, from 1990 to 1995. He was a reader in computer science at

Queen Mary University of London Queen Mary University of London (QMUL, or informally QM, and formerly Queen Mary and Westfield College) is a public university, public research university in Mile End, East London, England. It is a member institution of the federal University ...

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

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

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 researcher at Meta AI (FAIR) 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 Fellowship, known as the Royal Society Wolfson Research Merit Award until 2020, is a 5 years fellowship awarded by the Royal Society since 2000. The scheme is described by the Royal Society as providing ''long-term flexib ...

. 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 Scholarship, fellowship for engineers who are recognised by the Royal Academy of Engineering as being the best and brightest engineers, inventors and technologists in United K ...

(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 Fellows 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 Laws (LL.D.) is a doctoral degree in legal studies. The abbreviation LL.D. stands for ''Legum Doctor'', with the double “L” in the abbreviation referring to the early practice in the University of Cambridge to teach both canon law ...

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. He was named as an

ACM Fellow ACM Fellowship is an award and fellowship that recognises outstanding members of the Association for Computing Machinery (ACM). The title of ACM Fellow A fellow is a title and form of address for distinguished, learned, or skilled individuals ...

, in the 2024 class of fellows, "for contributions to the science and engineering of reasoning about programs".

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 2024 fellows of the Association for Computing Machinery