Testing the Satisfiability of Formulas in Separation Logic with Permissions
Nicolas Peltier · Lecture notes in computer science · 2023
Abstract We investigate the satisfiability problem for a fragment of Separation Logic (SL) with inductively defined spatial predicates and permissions. We show that the problem is undecidable in general, but decidable under some restrictions on the rules defining the semantics of the spatial predicates. Furthermore, if the satisfiability of permission formulas can be tested in exponential time for the considered permission model then SL satisfiability isExptimecomplete.