Email: portico-services@ucl.ac.uk
Help Desk: http://www.ucl.ac.uk/ras/portico/helpdesk
- 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.


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.