Separation Logic (SL) enables reasoning about programs that manipulate pointers. Its key feature is the separating conjunction ⋆, which asserts that two formulas hold on disjoint portions of memory. We consider an extension of SL, called Overlaid SL (OSL), that allows non-disjoint combinations of data structures defined over different fields, enriched with set constraints on the nodes of these structures. We prove that entailment is decidable for a broad class of data structures satisfying the so-called PCE conditions of [Iosif et al., 2013], thus extending this result to OSL. Our decision procedure is nondeterministic with doubly exponential time complexity.

International audience