Professor of Computer Science
Royal Society Wolfson Research Merit Award Holder
Member of Theory Research Group
Address: Department of Computer Science, Queen Mary, University of London, London, E1 4NS, UK
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.
With John Reynolds (CMU)
I developed separation logic, which addresses the problem of tractable reasoning
about programs that use pointers.
With David Pym (then at Queen Mary, now at HP) I developed
bunched logic,
a general logic of resource, which
is a more abstract
cousin of and precursor to separation logic.
In recent years
I've been tempted into tools research
where I help out, or get dragged along by, many
excellent colleagues in the London/Cambridge area
who are enthusiastically
pursuing mechanized program verification and static program analysis.
This particularly involves the SpaceInvader team (Cristiano Calcagno,
Dino Distefano, Hongseok Yang and me) in London
and our SLAyer/TERMINATOR colleagues at Microsoft Cambridge (Josh Berdine,
Byron Cook).
Research Links:
East London Massive
Separation Logic
Papers
Students and RAs
Tool Projects:
Smallfoot
SpaceInvader Blog
SLAyer
Terminator