Undecidability of Propositional Separation Logic and Its Neighbours

Separation logic has proven an effective formalism for the analysis of memory-manipulating programs. We show that the purely propositional fragment of separation logic is undecidable. In fact, for any choice of concrete heap-like model of separation logic, validity in that model remains undecidable. Besides its intrinsic technical interest, this result also provides new insights into the nature of decidable fragments of separation logic. In addition, we show that a number of propositional systems which approximate separation logic are undecidable as well. In particular, these include both Boolean BI and Classical BI. All of our undecidability results are obtained by means of a single direct encoding of Minsky machines.