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, 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.
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.