O'Hearn is best known for separation logic, a theory he developed with John C. Reynolds that unearthed new domains for scaling logical reasoning about code. This built upon previous research from O'Hearn and David Pym on logic for resources — Bunched logic. With Stephen Brookes, Carnegie Mellon University, O'Hearn created Concurrent Separation Logic, extending the theory further. Tony Hoare, in discussing the grand challenge of program verification, described CSL as "solving two problems...concurrecy and object orientation". Separation logic has given rise to the Infer Static Analyzer, a static program analysis utility developed by O'Hearn's team at Facebook. After 20 plus years in academia, O'Hearn landed 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, Spotify, Mozilla, Uber, 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 in computer science at Queen Mary University of London from 1996 to 1999 and then a full professor at Queen Mary until his move to University College London. At UCL he was granted a Royal Academy of Engineering/Microsoft Research Chair. In 1997 he was a visiting scientist at Carnegie Mellon University and in 2006 he was a visiting researcher at Microsoft Research Cambridge.. He now shares his time working as a research scientist at Facebook and a professor at UCL.
Awards and honours
In 2007, O'Hearn was granted a Royal Society Wolfson Research Merit Award. 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, for the invention of Concurrent Separation Logic. Also in 2016, he was elected Fellow of the Royal Academy of Engineering and co-received the annual CAV award. In 2018, he was elected Fellow of the Royal Society, and was bestowed with an Honorary Doctor of Laws from Dalhousie University.. January 2019 saw O'Hearn honoured with another Most Influential POPL Paper Award, which he shared with three colleagues.
