Concurrency
One of the largest research challenges in formal methods is finding
compositional development methods
to cope with systems which run in concurrent environments.
This challenge becomes ever more pressing with the advent of many-core hardware.
My Oxford research showed how the notion of interference could be
handled in specifications and design verification by using rely and guarantee-conditions
(the two publications
Specification and design of (parallel) programs;
Development Methods for Computer Programs including a Notion of Interference
between them show over 600 citations in Google Scholar(2012) and even my thesis records over 200 citations).
An Annotated list of rely/guarantee publications is
available (but is in serious need of revision!).
This research (complemented theses by Ketil Stoelen, Xu Qiwen and Pierre
Collette) has proved successful and has led to a significant amount
of recent research .
It is however true that rely/guarantee reasoning is heavier than for sequential programs
and the "pobl" research (Parallel Object-Based Language) is based on the
observations that -for relatively simple concurrent programs- it is possible
to use object-oriented concepts in order to constrain the interference
which is possible and to virtually eliminate the necessity to reason directly
about interference.
The most useful references on the "pobl" work are:
-
Accommodating Interference in the Formal Design of Concurrent Object-Based Programs
Cliff B. Jones;
Formal Methods in System Design,
Vol 8, No 2, pp105-122.
-
Non-Interference Properties of a Concurrent Object-Based Language:
Proofs Based on an Operational Semantics
Steve J. Hodges and Cliff B. Jones in Oject Orientation with Parallelism
and Persistence, Kluwer Academic Publishers 1996. Editors: Burkhard
Freitag, Cliff B. Jones, Christian Lengauer and Hans-Joerg Schek.
-
Process Algebra Arguments about an Object-Based Design Notation
C. B. Jones in A Classical Mind, Prentice-Hall 1994. Editor:
A. W. Roscoe.
We also had an EPSRC-funded project ("Splitting (software) atoms safely")
that looked at Atomicity Refinement funded by EPSRC.
In some sense, this is a developmental view of "linearizability".
A couple of key publications here are:
Current research on concurrency includes looking at the links to separation logics -
recent cooperation with
Ian Hayes looks extremely promising.
Some references are: