Brief Bio (composed with the help of Meta AI)
Peter O'Hearn is a researcher at Meta AI and a Professor at University College London. He has made significant contributions to programming languages, logic, and software verification. Peter developed Separation Logic and Incorrectness Logic, theories which have been used in various reasoning tools, including Infer, a program analyzer that has detected hundreds of thousands of bugs at Facebook and other companies. Prior to joining Meta, Peter co-founded Monoidics, a verification startup that developed Infer and was acquired by Facebook in 2013. Peter has received numerous awards for his work, including the Godel Prize and being elected a Fellow of the Royal Society.
Longer Bio
Peter O'Hearn is a researcher at Meta AI and a
Professor at University College London.
Peter has done research in
the broad areas of programming languages and logic,
and held academic
positions at Syracuse University, Queen Mary University of London, and University College London, and he worked at Facebook from 2013-2021; he joined FB with
the acquisition of the verification startup Monoidics.
After a stint at Lacework, Peter returned to `Meta in 2024 to work with the
FAIR (Fundamental AI Research) team.
With David Pym, Peter developed Bunched Logic, a general logic of resources. BI was then used in
Separation Logic, developed in joint work with
John Reynolds and others, a theory which opened up new practical possibilities for program proof, including the technology which led to the Infer program analyzer developed by Peter's team at Facebook. Infer runs internally on Facebook's code bases, and has detected hundreds
of thousands of bugs which have been fixed by Facebook's developers before reaching products.
Infer is also used in production at number of other companies, including Amazon,
Microsoft and Mozilla, and is deployed to many other organizations
through the Sonatype Lift analysis platform.
Most recently Peter developed Incorrectness Logic,
a theory aimed at providing a foundation for bug catching tools based
on proofs of the presence of bugs. Peter is a Fellow of the Royal Society (elected 2018), a Fellow of the Royal Academy of Engineering (2016), he
has received a number of awards for his work including the the 2016 G\"odel Prize, the 2016 CAV Award, the 2021 IEEE Cybersecurity Award for Practice, he has received test-of-time awards for papers in POPL (2001 and 2009 papers) and CONCUR (2004 paper), and he
received an honorary doctorate from Dalhousie University in 2018.