A Reachable Star

 

Etienne Lozes (LSV Cachan, F)

 

Abstract:

 

Separation Logic is both an assertion language that may express some
properties of memory states, and a Hoare-like proof system for
programs manipulating pointers, the former being intensively used in
the latter.  This logic has been actively popularized by the "London
Massive" team (Peter O'Hearn, Hongseok Yang, Cristiano Calcagno, Dino
Di Stefano).

In the first part of my presentation, I will present a personnal,
brief survey on pointer programs verification, and introduce the
essentials of the separation logic approach. The second part will be
more personnal and technical, I will focus on the assertion language
and review some of our recent results on decidability and
expressiveness issues.

On the decidability side, I will present decidable classes that are
not (yet) handled by the automatic tools developed by the "London
Massive" team : data-aware logics, and unrestricted first-order
quantification.  This results allow to prove, for instance, that
merging two ordered lists gives an ordered list.

On the expressiveness side, I will explain the roles played by the two
specific separation logic connectives : separating conjunction and
magic-wand (joint work with St?phane Demri and Remi Brochenin).  It
will be presented in particular that the magic-wand subsumes the
separating conjunction, and provides an expressive power equivalent to
*full* second-order logic. Of other interest is that separating
conjunction alone fits into *monadic* second-order logic, the strict
inclusion being still a conjecture, although it is known that it
encodes MSO over words.