PeopleofSuperintelligence

Researcher

Peter O'Hearn

Also known as Peter W O'Hearn, Peter William O'Hearn

Peter O'Hearn is a computer scientist whose logics for reasoning about programs became industrial bug-finding tools, and who now works on language models and code reasoning at Meta. He earned a PhD at Queen's University in 1991, held posts at Syracuse University and Queen Mary University of London, and developed bunched logic with David Pym. He co-founded Monoidics in 2009, and after Facebook acquired the startup in 2013, he and colleagues open-sourced the Infer static analyzer in 2015. He shared the 2016 Gödel Prize with Stephen Brookes for Concurrent Separation Logic, became a Fellow of the Royal Society in 2018 and an ACM Fellow in 2024. After leading Code Security development at Lacework from 2021 to 2024, he returned to Meta's AI team in 2024; he is a researcher at Meta Superintelligence Labs and a professor at University College London.

Born
1963
Works
223
Citations
9,962
h-index
49
Badges

Years link to their sources. Publication numbers from OpenAlex, as of 22 October 2026.

Timeline

  1. 1985–1999

    Degrees, Syracuse and Queen Mary

    He earns a BSc in computer science from Dalhousie University in 1985, then an MSc in 1987 and a PhD in 1991 at Queen's University in Kingston, Ontario, with Robert D. Tennent as his doctoral advisor. From 1990 to 1995, he is an assistant professor at Syracuse University, and from 1996 to 1999 he is a reader in computer science at Queen Mary University of London.

  2. 2001–2012

    Bunched logic and a UCL chair

    In 2001, he and Samin Ishtiaq present BI as an Assertion Language for Mutable Data Structures at POPL, linking the bunched logic he developed with David Pym in the 1990s to the problem of programs misusing memory. POPL gives the paper its Most Influential Paper award in 2011. In 2012, he receives the Royal Academy of Engineering/Microsoft Research Chair at University College London.

  3. 2009–2015

    Monoidics and Facebook Infer

    He co-founds the software company Monoidics in 2009, which develops the Infer static analyzer, and he takes a position at Facebook in 2013 when Facebook acquires it. In June 2015, he, Dino Distefano and Cristiano Calcagno open-source Facebook Infer, a static program analyzer that finds bugs such as null pointer access and resource and memory leaks in mobile code before it ships.

  4. 2016–2018

    Gödel Prize and Royal Society

    In 2016, he and Stephen Brookes receive the Gödel Prize for their invention of Concurrent Separation Logic, and he is elected a Fellow of the Royal Academy of Engineering. In 2018, he is elected a Fellow of the Royal Society.

  5. 2021–2024

    Code security at Lacework

    After Facebook, where he works from 2013 to 2021, he moves to the cybersecurity company Lacework and leads development of its Code Security product until 2024.

  6. 2024

    An ACM Fellow

    ACM names him a Fellow in its 2024 class for contributions to the science and engineering of reasoning about programs.

  7. 2024–2026

    LLM reasoning work at Meta

    He returns to Meta in 2024 to join its AI team. In February 2025, he coauthors Logic.py with Pascal Kesseli and Ricardo Silveira Cabral: a language model formalises each logic puzzle in a domain-specific language and a constraint solver solves it, a 65% absolute improvement over Llama 3.1 70B alone, to over 90% accuracy on ZebraLogicBench. With Mark Harman and Shubho Sengupta, he gives the FSE 2025 keynote on LLM-based software testing, and in January 2026 he coauthors a study in which GPT-5 and Claude Sonnet 4.5 score comparably to top-ranked verification tools on program termination, with test-time scaling.

  8. As of October 2026

    Meta Superintelligence Labs and UCL

    He is a researcher at Meta Superintelligence Labs and a professor at University College London, with interests in reasoning for code and for other-than-code. He is a member of the Royal Society's Sectional Committee for computer sciences from September 2025 to September 2028.

Career

  1. Since 2012University College LondonProfessor
  2. NowMeta Superintelligence LabsResearcher
  3. 2021–2024LaceworkCode Security development lead
  4. 2013–2021Meta
  5. 2009–2013MonoidicsCo-founder
  6. 2002–2009University of London
  7. 1996–1999Queen Mary University of LondonReader in Computer Science
  8. 1990–1995Syracuse UniversityAssistant Professor

Education

  1. 1991Queen's UniversityPhD
  2. 1987Queen's UniversityMSc
  3. 1985Dalhousie UniversityBSc in computer science

From the biography and OpenAlex affiliations (the years of papers that list the organization), so some years are approximate.

Most-cited works

  1. Local Reasoning about Programs that Alter Data Structures2001 · Lecture notes in computer science · 706 citations
  2. Resources, concurrency, and local reasoning2007 · Theoretical Computer Science · 552 citations
  3. BI as an assertion language for mutable data structures2011 · ACM SIGPLAN Notices · 489 citations
  4. The Logic of Bunched Implications1999 · Bulletin of Symbolic Logic · 472 citations
  5. Permission accounting in separation logic2005 · ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) · 370 citations

From OpenAlex, as of 21 October 2026.

  1. The median h-index is 48 at universities and 14 at frontier AI labsIncludes Peter O'Hearn. The median h-index is 48 at universities and 14 at frontier AI labs. We compare publishing careers, recent citations, dual appointments and job moves across 2,420 university researchers and 308 frontier-lab researchers.
  2. The Massachusetts Institute of Technology trained or employed 44 of the 187 AI major-prize winners, more than any other universityIncludes Peter O'Hearn. The Massachusetts Institute of Technology trained or employed 44 of the 187 AI major-prize winners, more than any other university. We compare doctorate and 5+ year employment links, career timing and current workplaces for 187 major-prize and 1,111 best-paper winners.
  3. 11% of AI doctorate holders from 2010 to 2016 founded or led a company or lab by 10 years after graduationIncludes Peter O'Hearn. We estimate how often AI doctorate holders founded or led a company or lab by 10 years after graduation, how waiting times compare between founders and top jobs, and which universities trained the most.
  4. The company share of AI researchers’ top papers was 31% in 2020–2024 and 8% in 1970–1974Includes Meta. We estimate where the people shaping AI worked when their most-cited papers appeared: the company share was 31% in 2020–2024 and 8% in 1970–1974, and Google led all organizations in 2020–2024.

Colleagues

People with dated positions at the same organization in the same years.

Sources and credits

Photo: We have no published photo of Peter O'Hearn yet. Send us a free-licensed photo.

  1. Peter O'Hearn - Wikipedia en.wikipedia.org. Checked 20 October 2026.
  2. Computer Science professor wins prestigious award - Queen Mary University of London qmul.ac.uk. Checked 20 October 2026.
  3. Introducing Dal's honorary degree recipients for Spring Convocation 2018 - Dalhousie University dal.ca. Checked 20 October 2026.
  4. Professor Peter O'Hearn FREng FRS - Royal Society royalsociety.org. Checked 20 October 2026.
  5. Open-sourcing Facebook Infer: Identify bugs before you ship - Engineering at Meta engineering.fb.com. Checked 20 October 2026.
  6. 2016 Gödel Prize - EATCS eatcs.org. Checked 20 October 2026.
  7. Keynote: Underapproximate Reasoning at Scale - Science of Security Virtual Organization sos-vo.org. Checked 20 October 2026.
  8. Logic.py: Bridging the Gap between LLMs and Constraint Solvers - arXiv arxiv.org. Checked 20 October 2026.
  9. Harden and Catch for Just-in-Time Assured LLM-Based Software Testing: Open Research Challenges - arXiv arxiv.org. Checked 20 October 2026.
  10. LLMs versus the Halting Problem: Characterizing Program Termination Reasoning - arXiv arxiv.org. Checked 20 October 2026.
  11. Peter O'Hearn - UCL Computer Science www0.cs.ucl.ac.uk. Checked 20 October 2026.