Peter O'Hearn

Professor of Computer Science & EPSRC Advanced Fellow
Department of Computer Science
Queen Mary, University of London
London E1 4NS
Phone: +44 (0)20 7882 5443;   Fax: +44 (0)20 8980 6533;   e-mail: ohearn AT dcs.qmul.ac.uk

My research interests are in logic and semantics of computation, both the foundations and applications thereof. Most recently this has concentrated on local reasoning , where a specification and proof can concentrate on a circumscribed collection of resources that a program actually acts upon, instead of the entire global state of a system. The key tools underlying this project are the logic of bunched implications, developed with David Pym, and separation logic, developed with John Reynolds, Hongseok Yang, and others.

  East London Massive     Information on Local Reasoning and Separation Logic     Online Papers     Students and Colleagues

• Program Analysis with Separation Logic .
  • A local shape analysis based on separation logic
    D Distefano, P O'Hearn and H Yang. To appear in TACAS'06.
• Smallfoot . Smallfoot is an experimental tool for checking certain lightweight separation logic specifications.
  • Smallfoot v0.1 release, 15-12-2005
  • Modular Automatic Assertion Checking with Separation Logic
    J Berdine, C Calcagno and PW O'Hearn. Draft of November 2005. A technical appendix with variable conditions.
  • A Collection of Example Programs
• Separation Logic for Concurrency . Quite a lot of recent interest surrounds concurrency. Some highlights: we can transfer portions of heap between processes, as in a resource manager or in efficient message passing; we can do modular reasoning in the presence of semaphores (e.g., split binary semaphores without maintaining a global invariant); we do parallel mergesort with no rely or guarantee conditions, the proven processes automatically mind their own business.
  • Resources, Concurrency and Local Reasoning , PW O'Hearn, to appear in Theoretical Computer Science
    A preliminary version appeared in the Proceedings of CONCUR'04, LNCS 3170, pp49-67.
  • The Smallfoot Assertion Checker automatically does some proofs in the concurrent logic.
  • A Semantics for Concurrent Separation Logic , SD Brookes, Proceedings of CONCUR'04, LNCS 3170, pp16-34.
  • Permission Accounting in Separation Logic, by R Bornat, C Calcagno, P O'Hearn and M Parkinson, POPL 2005, 59-70.
  • Steve Brookes and I gave a joint tutorial at CONCUR'04 .
  • Here are slides from my invited talk at ETAPS'04 .

  Film

  Attack of the 50 Foot Spatial Dudes

  Proof of Cyclic List Reversal

  ---