Abstract

In this talk, I will present a decision procedure for a fragment of separation logic (SL) with arbitrary nesting of separating conjunctions with boolean conjunctions, disjunctions, and guarded negations together with a support for the most common variants of linked lists. The method is based on a model-based translation to SMT for which we introduce several optimisations–the most important of them is based on bounding the size of predicate instantiations within models of larger formulae, which leads to a much more efficient translation of SL formulae to SMT. I will also briefly discuss ongoing research to generalise the decision procedure for user-defined inductive predicates.