Habilitation à diriger des recherches
Etienne Lozes


Separation Logic: Expressiveness and Copyless Message-Passing

Check out the memory
Have a look at the slides

Date and place

Tuesday, July 3rd 2012 at 2pm30 (WARNING: time changed).
Salle de Conférences, Pavillon des Jardins, École Normale Supérieure de Cachan.

How to reach ENS Cachan
How to reach pavillon des jardins



My habilitation centers on separation logic, a program logic introduced by O'Hearn, Reynolds and Yang in 2001 for reasoning modularly about heap-manipulating programs.

The first part of my habilitation addresses the question of the expressive power of the assertion language of Separation Logic. This question is of particular importance for the automation of the verification or inference of a program's proof. Recent techniques based on bi-abduction are intimately related to one of the most intriguing features of Separation Logic, the so-called "magic wand" logical connector. Some years ago, I showed that in some situations it was possible to eliminate this operator, and to reduce Separation logic to a propositional logic. This result holds for a Separation Logic without quantifiers over memory locations. The habilitation presents recent advances that show a much more mitigated picture, and tries to better explain some of the reasons why symbolic heaps, the fragment of Separation Logic that got adopted by some of the program provers, is a sensible one.

The second part of my memory develops an extension of the proof system of Separation Logic for Hoare triples. This extension is dedicated to copyless message passing, a form of message passing that takes advantage of a shared memory to reduce the amount of copies involved along message exchanges. Inspired by the Sing# operating system, the proof system introduces channel contracts, which specify for each communication channel the protocol that should be followed on that channel. The theory of these communication contracts is exposed, in particular its connection to half-duplex communicating finite state machines. The proof system is shown to enforce several properties on provable programs, some of which are rather standard in Separation Logic, like memory safety, or race-freedom, and others that are possibly less expected, like some special forms of deadlock-freedom, or the confluence of computations.

About LSV