Undecidability of propositional separation logic and its neighbours

James Brotherston

Department of Computing
Imperial College London

Thursday, 17 November 2011, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf]

Abstract: Separation logic has become well-established in recent years as an effective formalism for reasoning about memory-manipulating programs. In this talk I shall explain why separation logic is undecidable even at the purely propositional level. In fact, it turns out this is generally the case no matter whether we consider validity in a particular heap model, validity in a class of models, or provability in an axiomatisation based on Boolean BI or Classical BI. All of these results are new, and some were considered open problems for some time. Our undecidability results also yield new insights into the necessary limitations on decidable fragments of separation logic.

(Joint work with Max Kanovich, Queen Mary, University of London, published in LICS 2010.)

ERDF
Tarmo Uustalu
Last update 5.2.2012