UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

Undecidability of propositional separation logic and its neighbours

Brotherston, J; Kanovich, M; (2010) Undecidability of propositional separation logic and its neighbours. In: (pp. pp. 130-139).

Full text not available from this repository.


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. © 2010 IEEE.

Type: Proceedings paper
Title: Undecidability of propositional separation logic and its neighbours
ISBN-13: 9780769541143
DOI: 10.1109/LICS.2010.24
UCL classification: UCL > School of BEAMS
UCL > School of BEAMS > Faculty of Engineering Science
URI: http://discovery.ucl.ac.uk/id/eprint/1353143
Downloads since deposit
Download activity - last month
Download activity - last 12 months
Downloads by country - last 12 months

Archive Staff Only

View Item View Item