An Entailment Checker for Separation Logic with Inductive Definitions

Abstract

In this paper, we present Inductor, a checker for entailments between mutually recursive predicates, whose inductive definitions contain ground constraints belonging to the quantifier-free fragment of Separation Logic. Our tool implements a proof-search method for a cyclic proof system that we have shown to be sound and complete, under certain semantic restrictions involving the set of constraints in a given inductive system. Dedicated decision procedures from the DPLL(T)-based SMT solver CVC4 are used to establish the satisfiability of Separation Logic formulae. Given inductive predicate definitions, an entailment query, and a proof-search strategy, Inductor uses a compact tree structure to explore all derivations enabled by the strategy. A successful result is accompanied by a proof, while an unsuccessful one is supported by a counterexample.