Abstract Separation logic (SL) is extensively employed in verification to analyse programmes that manipulate dynamically allocated memory. The entailment problem, when dealing with inductively defined predicates or data constraints, is undecidable for SL formulas. Our focus is on addressing a specific fragment of this issue, wherein the consequent is restricted to clauses of some particular form, devoid of inductively defined predicates. We present an algorithm designed to determine the validity of such entailments and demonstrate that the problem is decidable and ExpTime complete under some conditions on the data theory. This algorithm serves the purpose of verifying that the data structures outlined by a given SL formula (the antecedent) adhere to certain shape constraints expressed by the consequent.
Nicolas Peltier (Mon,) studied this question.