On the Almighty Wand

10 years 7 months ago
On the Almighty Wand
We investigate decidability, complexity and expressive power issues for (first-order) separation logic with one record field (herein called SL) and its fragments. SL can specify properties about the memory heap of programs with singly-linked lists. Separation logic with two record fields is known to be undecidable by reduction of finite satisfiability for classical predicate logic with one binary relation. Surprisingly, we show that second-order logic is as expressive as SL and as a by-product we get undecidability of SL. This is refined by showing that SL without the separating conjunction is as expressive as SL, whence undecidable too. As a consequence of this deep result, in SL the magic wand can simulate the separating conjunction. By contrast, we establish that SL without the magic wand is decidable with non-elementary complexity by reduction from satisfiability for the first-order theory over finite words. Equivalence between second-order logic and separation logic extends to the...
Rémi Brochenin, Stéphane Demri, &Eac
Added 19 Oct 2010
Updated 19 Oct 2010
Type Conference
Year 2008
Where CSL
Authors Rémi Brochenin, Stéphane Demri, Étienne Lozes
Comments (0)