Institutional Research Information Service
UCL Logo
Please report any queries concerning the funding data grouped in the sections named "Externally Awarded" or "Internally Disbursed" (shown on the profile page) to your Research Finance Administrator. Your can find your Research Finance Administrator at https://www.ucl.ac.uk/finance/research/rs-contacts.php by entering your department
Please report any queries concerning the student data shown on the profile page to:

Email: portico-services@ucl.ac.uk

Help Desk: http://www.ucl.ac.uk/ras/portico/helpdesk
 More search options
Prof Peter O'Hearn
Prof Peter O'Hearn profile picture
  • Professor of Computer Science
  • Dept of Computer Science
  • Faculty of Engineering Science

Peter O'Hearn is a Professor of Computer Science at University College London, where he heads the Programming Principles, Logic and Verification research group.

Peter has done research spanning from program semantics and mathematical logic through to automated tools for program verification and analysis. He developed Separation Logic with John Reynolds, addressing the problem of tractable reasoning about programs that mutate memory, and this led to his further work on Concurrent Separation Logic and on the software tools Smallfoot, Space Invader and Abductor for analyzing programs with mutable data.

Peter did his PhD at Queen's University in Kingston, Ontario, Canada, under the supervision of Bob Tennent. His thesis work (completed, 1991) uncovered some of the semantic structure (doubly-closed categories) that would later resurface in separation and bunched logics. Peter held academic positions at Syracuse (1991-1995) and Queen Mary (1996-2012), before moving to UCL in March of 2012. From 2003-2009 he was supported by an EPSRC Advanced Research Fellowship. Peter received a Royal Society Wolfson Research Merit Award in 2007. In 2011 he received the Most Influential POPL Paper Award, a retrospective award given annually for a paper published at the ACM/SIGPLAN Principles of Programming Languages symposium 10 years earlier. Peter currently holds a Royal Academy of Engineering/Microsoft Research Chair in Logic and Software Verification at UCL.

Research Groups
Research Summary

My research interests are in logic and semantics of computation, and in automated tools for program verification and analysis.

With John Reynolds I developed separation logic, which addresses the problem of tractable reasoning about the mutation of data structures in computer memory. With David Pym I developed bunched logic, a general logic of resource, which is a more abstract cousin of and precursor to separation logic. I proposed a concurrent separation logic, which has made inroads on the problem of modular reasoning about shared-memory concurrent programs.

In much of my work I have been interested in the concept of locality, the idea that programmers look at state in little pieces rather than keeping track of the entire global state. I proposed a connection between parametric polymorphism and local state in a JACM'95 paper with Bob Tennent. This spurred some of my later work on separation logic and the frame problem and what I called "local reasoning", that you can reason about a piece of code by talking only about the resources it touches instead of tracking the entire global state of a system.

In recent years I've gotten involved in software tools research, particularly with the SpaceInvader team (Cristiano Calcagno, Dino Distefano, Hongseok Yang and I) when we were all in London and our SLAyer/TERMINATOR colleagues at Microsoft Cambridge (Josh Berdine, Byron Cook). Eventually, the local reasoning idea was ported to program analysis, by using a variation on abductive inference to approximate a program's footprint, and this allowed a certain kind of automatic program analysis to scale to millions lines of code, where previously only hundreds or a few thousands were possible (see new JACM'11 bi-abduction paper).

Of late I've also been paying attention to some of the fascinatingly intricate fine-grained concurrent algorithms, and to abstract models of consurrency. Despite decades of work, there are absolutely basic, unsolved problems in concurrency, and the problems are becoming all the more urgent because of developments in chip design.

Concurrency and automated analysis are both vibrant research areas, with unsolved, basic problems, and this is where my main current interests lie. There is a tremendous amount of work to be done in both of these areas. And when one combines the two, analyzing or verifying concurrent programs, the problems become even harder, which is to say as well more interesting. StatCounter - Free Web Tracker and Counter

Teaching Summary
I have taught extensively, previously, at Syracuse and Queen Mary universities. I don't have teaching commitments at the moment because I am on a RAEng/Microsoft Research Chair.
Some IRIS profile information is sourced from HR data as explained in our FAQ. Please report any queries concerning HR data shown on this page to hr-services@ucl.ac.uk.
University College London - Gower Street - London - WC1E 6BT Tel:+44 (0)20 7679 2000

© UCL 1999–2011

Search by