John C. Reynolds gave a brief presentation on Separation logic,
an extension of Hoare logic for reasoning about shared mutable
data structres that was discovered independently by him and
Peter O'Hearn.

A simple example of the advantage of the logic is the invariant
of a program for in-place reversal of a list.  In Hoare logic,
one would have to write

   Exists x,y. list x i and list y j 
      and compose(reflect(y),x) = x0
      and forall k. reachable i k and reachable j k
                                        implies k = nil

where list x i asserts that i is a list representing the
sequence x, and the final conjunct asserts that only nil
is reachable from both i and j, i.e. that the lists i and j
do not share storage.

In separation logic, however, one can write

   Exists x,y. (list x i * list y j)
            and compose(reflect(y),x) = x0

where * is a "separating conjunction" that asserts that its
components hold for disjoint areas of storage.

A central feature of the logic is the "frame rule":

     {p}c{q}
   -----------  when c assigns to no variable free in r.
   {p*r}c{q*r}

Using this rule, one can limit the proof of a program
fragment c to a specification {p]c{q} that only describes
the storage actually used by c, and then infer that c will
leave unchanged any property r of a disjoint storage area.

The setting of separation logic is a low-level imperative
programming language without garbage collection.  All proofs
preclude any dereferencing of dangling pointers.  It is also
possible to prove the absence of memory leaks, say by proving

   {p and empty}c{q and empty}

where empty asserts that the heap storage is empty.

The accomplishments of separation logic include the specification
and (manual) proof of the Schorr-Waite marking algorithm and the
Cheney copying garbage collector, as well as numerous simpler
programs.  There is also an extension of the logic to shared-
variable concurrency which is capable of treating, for example,
processes that communicate storage ownership through a shared
buffer, or concurrent quicksort.  A further extension permits
read-only sharing via Boyland's fractional permissions.

Reynolds refused to claim that any problems were "nearly solved"
(since such a claim once boomeranged on him).  As unsolved
problems, he mentioned data structures with rich sharing, such
as cyclic graphs, the need to move towards richer programming
languages, and the need for automation.

He provided the following list of researchers in the area:

   London:          Peter O'Hearn
                    Richard Bornat
                    Samin Ishtiaq
                    Cris Calcagno
                    Josh Berdine
                    Ivana Mijajlovic
                    Dino DeStefano

   Cambridge (UK):  Matthew Parkinson
                    Gavin Bierman

   Copenhagen:      Lars Birkedal
                    Noah Torp-Smith
                    Bodil Biering

   Seoul:           Hong Seok Yang

   Pittsburgh:      John Reynolds
                    Aleks Nanevski