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: Proceedings - Symposium on Logic in Computer Science. (pp. 130 - 139).

Full text not available from this repository.

Abstract

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
DOI:10.1109/LICS.2010.24
UCL classification:UCL > School of BEAMS > Faculty of Engineering Science > Computer Science

Archive Staff Only: edit this record