Peter O'Hearn

• Algebra, Logic, Locality, Concurrency. Slides from APLAS/CPP joint invited talk, Kenting, Taiwan, December 2011.
• Compositional Shape Analysis by means of Bi-Abduction. Journal of the ACM (JACM), Volume 58 Issue 6, December 2011. 73 pages.
  C Calcagno, D Distefano, PW O'Hearn and H Yang.
  This extended version of the POPL'09 abduction paper has lots of new material, in particular where the static analysis alrogithms are described in "model checking style" with a worlkist algorithm, rather than in "denotational semantics style".
• Marktoberdorf Summer School Lectures.
• On Locality and the Exchange Law for Concurrent Processes.
  CAR Hoare, A Hussain, B Moller, PW O'Hearn, RL Petersen and G Struth. CONCUR 2011
• The Complexity of Abduction for Separated Heap Abstractions.
  N Gorogiannis, M Kanovich and PW O'Hearn. SAS 2011

Research:    

My research interests are in logic and semantics of computation. With John Reynolds (CMU) I developed separation logic, which addresses the problem of tractable reasoning about the mutation of data structures in computer memory. With David Pym (then at Queen Mary, now at Abereen) 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 (proven sound by Steve Brookes), 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) 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 paper under News). Of late I've also been paying attention to some of the fascinatingly intricate fine-grained concurrent algorithms (Bornat, Rinetzky, Yang..). More generally, I have many excellent colleagues in the London/Cambridge area who are enthusiastically pursuing program logic and semantics, mechanized program verification and static program analysis; it is a great place for this sort of research at the moment.

Random Links (includes past and present):     Publications     Resource Reasoning     TCS@QM     Separation Logic     Smallfoot     SLAyer     Terminator     Attack of the 50 Foot Spatial Dudes     Proof of Cyclic List Reversal