Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456 Peter O'Hearn
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.
I am fascinated by the idea of
local reasoning, where
reasoning concentrates
on a circumscribed collection of
resources that a program actually acts upon.
It could hold the key to scalable reasoning,
but it is extremely
challenging because of possible ``bugs at a distance''
which threaten to make local reasoning unsound.
The key tools that enabled a first technical push in this direction are
the logic of bunched implications,
developed with David Pym, and separation logic, developed with John Reynolds,
Hongseok Yang, and others.
The East London Massive that I work with
has begun a
foray into tools for
mechanized reasoning and
automatic program analysis, as represented by Smallfoot, Space Invader,
Terminator and SLAyer.
SeparationFest, 18 July 2007.
John Reynolds is receiving an honorary degree from Queen Mary on
17 July, and we are taking the opportunity to have a day of talks
related to separation logic. Tony Hoare will be the keynote speaker.