A decision procedure for satisfiability in separation logic with inductive predicates
J G. Brotherston, Carsten Fuhs, Juan Antonio Pérez-Ortiz, Nikos Gorogiannis · 2014
We show that the satisfiability problem for the "symbolic heap" fragment of separation logic with general inductively defined predicates --- which includes most fragments employed in program verification --- is decidable. Our decision procedure is based on the computation of a certain fixed point from the definition of an inductive predicate, called its "base", that exactly characterises its satisfiability.