Résumé | Separation logic is a program logic à la Hoare that was introduced by Reynolds and O'Hearn at the end of the 90s.
Proving a program goes through writing valid Hoare triples {Pre} p {Post}, where Pre, Post are logical assertions and p is a program. The main novelty of separation logic with respect to Hoare logic is that the assertion language introduces two new logical connectives, the separating conjunction and the magic wand, and exploits them in some inference rules for Hoare triples. In the context of heap-manipulating programs, the assertion language can be seen as a special case of the spatial logic for graphs, where a graph property "A and separately B" means that the set of edges of the graph can be partitioned in two subsets such that the two resulting subgraphs satisfy A and B respectively. In this talk, after briefly reviewing the context of separation logic, I will compare separation logic and its fragments with weak second order and weak monadic second order logic. Separation logic will be shown to be equivalent to second order logic. It will also be shown that the magic wand subsumes the separating conjunction, in the sense that there is a logspace elimination procedure for separating conjunction (joint work with Remi Brochenin and Stephane Demri).
I will also report about a result due to Dawar and Antonopoulos that states that Separation logic without magic wand is strictly less expressive than monadic second order logic. |