Undecidability of propositional separation logic and its neighbours
File(s)DTR10-1.pdf (143.97 KB)
Published version
Author(s)
Brotherston, James
Kanovich, Max
Type
Report
Abstract
Separation logic has proven an adequate formalism for the
analysis of programs that manipulate memory (in the form
of pointers, heaps, stacks, etc.). In this paper, we consider
the purely propositional fragment of separation logic, as well
as a number of closely related substructural logical systems.
We show that, surprisingly, all of these propositional logics
are undecidable. In particular, we solve an open problem by
establishing the undecidability of Boolean BI.
analysis of programs that manipulate memory (in the form
of pointers, heaps, stacks, etc.). In this paper, we consider
the purely propositional fragment of separation logic, as well
as a number of closely related substructural logical systems.
We show that, surprisingly, all of these propositional logics
are undecidable. In particular, we solve an open problem by
establishing the undecidability of Boolean BI.
Date Issued
2010-01-01
Citation
Departmental Technical Report: 10/1, 2010, pp.1-10
Publisher
Department of Computing, Imperial College London
Start Page
1
End Page
10
Journal / Book Title
Departmental Technical Report: 10/1
Copyright Statement
© 2010 The Author(s). This report is available open access under a CC-BY-NC-ND (https://creativecommons.org/licenses/by-nc-nd/4.0/)
Publication Status
Published
Article Number
10/1