Deciding Satisfiability of Boolean Separation Logic with Inductive Predicates via Small Models

The authors present a novel decision procedure for a fragment of separation logic with arbitrary nesting of separating conjunctions, boolean conjunctions, disjunctions, and guarded negations, along with support for common variants of linked lists. The decision procedure is based on a model-based translation to SMT, with optimizations that bound the size of predicate instantiations within models, leading to an efficient translation.