Symbolic-Heap Separation logic (SHSL) is a popular formalism for automated reasoning about heap-manipulating programs, which allows the user to give customized data structure definitions. At the heart of formal proofs based on Separation Logic lies the entailment problem: Are all models of a formula also models of another formula?

While the entailment problem is undecidable for SHSL in general, various decidable fragments have been proposed. The most expressive of these fragments is due to Iosif, Rogalewicz and Simacek [1]. They prove decidability by a reduction to monadic second-order logic (MSO) over graphs of bounded tree-width. This gives rise to a decision procedure of non-elementary complexity. However, to the best of our knowledge, an actual entailment checker based on their approach has never been implemented.

In this paper, we give a new decidability proof for the SL fragment of Iosif, Rogalewicz and Simacek. We circumvent the reduction to MSO and give a direct model-theoretic construction with elementary complexity. We implemented our approach in the Harrsh analyzer and evaluate its effectiveness. In particular, we show that Harrsh can decide the entailment problem for data structure definitions for which no previous decision procedures have been implemented.

[1] Radu Iosif, Adam Rogalewicz, Jiri Simacek: The Tree Width of Separation Logic with Recursive Definitions (CADE 2013).