Radu Iosif
email: radu.iosif@univ-grenoble-alpes.fr

Cristina Serban
email: cristina.serban@univ-grenoble-alpes.fr

An Entailment Checker for Separation Logic with Inductive Definitions

Keywords: cyclic proofs, inductive definitions, infinite descent, separation logic AVoCS 2018

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.

Introduction

Inductive definitions play an important role in computing, being an essential component of programming languages, databases, automated reasoning and program verification systems. The main advantage of using inductive definitions is the ability of recursively reasoning about sets of logical objects. The semantics of these definitions is defined in terms of least fixed points of higher-order functions on assignments mapping predicates to sets of models. A natural problem is the entailment, that asks whether the least solution of one predicate is included in the least solution of another. Examples of entailments are language inclusion between finite-state (tree) automata, context-free grammars or verification conditions generated by shape analysis tools using specifications of recursive data structures as contracts of program correctness.

The interest for automatic proof generation is two-fold. On one hand, machine-checkable proofs are certificates for the correctness of the answer given by an automated checker, that increase our trust in the reliability of a particular implementation [SOR + 13]. On the other hand, the existence of a sound and complete proof system provides a (theoretical) decision procedure for the entailment problem. Assuming that the sets of models and derivations are both recursively enumerable, one can interleave the enumeration of counter-models with the enumeration of derivations; if the entailment holds one finds a finite proof (provided that the proof system is complete), or a finite counterexample, otherwise. Moreover, proof generation can be made effective by providing suitable strategies that limit the possibilities of applying the inference rules and guide the search towards finding a proof or a counterexample.

In this paper we consider inductive systems with constraints written in Separation Logic [START_REF] Reynolds | Separation Logic: A Logic for Shared Mutable Data Structures[END_REF] with the classical (strict) interpretation of spatial atoms. We introduce a set of inference rules tailored for proving inductive entailments in Separation Logic, which have been shown to be sound [START_REF] Iosif | Complete Cyclic Proof Systems for Inductive Entailments[END_REF] under a ranking assumption for the constraints of the inductive definitions. Completeness is assured under three additional restrictions and only for a particular interpretation of the least solution of the inductive system, taking into account the coverage trees of the heap generated by the inductive definitions. We then describe Inductor [START_REF] Serban | Inductor: an entailment checker for inductive systems[END_REF], a prototype implementation for the more general proof search algorithm given in [START_REF] Iosif | Complete Cyclic Proof Systems for Inductive Entailments[END_REF] and reprised in §2.4, and discuss several case studies involving both valid and invalid entailments.

Related Work

The problem of entailment in Separation Logic with inductive definitions has been approached by other solvers. The generic cyclic proof framework CYCLIST [START_REF] Brotherston | A Generic Cyclic Theorem Prover[END_REF] has an instantiation for this fragment and allows for the discovery of inductive arguments during proof construction. CYCLIST builds proofs in which infinite traces can be cut by induction when they satisfy a global trace condition requiring them to visit infinitely many progress points. SLEEK [START_REF] Chin | Automated Verification of Shape, Size and Bag Properties via User-defined Predicates in Separation Logic[END_REF] and SPEN [START_REF] Enea | A Solver for Separation Logic[END_REF][START_REF] Enea | On Automated Lemma Generation for Separation Logic with Inductive Definitions[END_REF] both provide methods of proving entailments by relying on lemmas that relate the inductive definitions. However, SLEEK utilizes a database of userprovided lemmas, while SPEN is able to automatically discover and synthesize concatenation lemmas.

Chu et al. [START_REF] Chu | Automatic Induction Proofs of Data-Structures in Imperative Programs[END_REF] propose a proof system that extends the basic cyclic proof method with a cut rule type that uses previously encountered sequents as inductive hypotheses and applies them by matching and replacing the left with the right-hand side of such a hypothesis. This method can prove entailments between predicates whose coverage trees differ and only soundness is guaranteed. An automata-based decision procedure that also tackles such entailments is given in [START_REF] Iosif | Deciding Entailments in Inductive Separation Logic with Tree Automata[END_REF]. This method translates the entailment problem to a language inclusion between tree automata and uses a closure operation on automata to match divergent predicates. Unlike proof search, this method uses existing tree automata inclusion algorithms, which do not produce proof witnesses.

2 Cyclic Proofs for Inductive Entailments in Separation Logic

Preliminaries

For two integers 0 ≤ i ≤ j, we denote by [i, j] the set {i, i + 1, . . . , j} and by [i] the set [1, i], where [0] = / 0. ||S|| denotes the cardinality of the finite set S. We consider a signature Σ = (Σ s , Σ f ), where Σ s is a set of sort symbols and Σ f is a set of function symbols. For the purpose of this paper, we restrict the signature such that Σ s = {Loc, Bool} and Σ f contains only equality, the constant symbol nil of sort Loc and the boolean constants and ⊥. Let Var be a countable set of first order variables, each x σ ∈ Var having a sort σ. We write x, y, . . . for both sets and ordered tuples of variables and, for brevity, we use ∈, ∪, ∩, ⊆ on tuples such that

x ∈ x iff x occurs in x, x ∪ y = {x | x ∈ x or x ∈ y}, x ∩ y = {x | x ∈ x and x ∈ y}, x ⊆ y iff x ∈ y for any x ∈ x.
A term t σ is either a constant or a variable of sort σ ∈ Σ s . Separation Logic (SL) formulae are generated by the following syntax:

ECEASST φ ::= | ⊥ | t σ 1 ≈ t σ 2 | emp | x Loc → (t Loc 1 , . . . ,t Loc k ) | φ 1 * φ 2 | ¬φ 1 | φ 1 ∧ φ 2 | φ 1 ∨ φ 2 | ∃x.φ 1 | ∀x.φ 1
where k > 0 is a fixed constant. Given a set of formulae F = {φ 1 , . . . , φ n }, we write * F for φ 1 * . . . * φ n , which is equivalent to emp if F = / 0. For a formula φ (set of formulae F), FV(φ) ( φ∈F FV(φ)) is the set of variables not occurring under a quantifier scope, and φ(x) (F(x)) means that, for every x ∈ x, we have x ∈ FV(φ) (x ∈ φ∈F FV(φ)).

Given sets of variables x and y, a flat substitution θ : x → y is a mapping of the variables in x to variables in y. We denote by xθ = {θ(x) | x ∈ x} its image under the substitution θ. For a formula φ(x), φθ is the formula obtained by replacing each occurrence of x ∈ x with the term θ(x). Observe that θ is always a surjective mapping between FV(φ) and FV(φθ). We lift this notation to sets as Fθ = {φθ | φ ∈ F}.

We fix an interpretation I such that I ( ) = true, I (⊥) = false, I (Loc) is a countably infinite set L, and I (nil) = nil is a fixed element of L. A valuation ν maps each variable x Bool to true or false and each variable y Loc to an element of L. Given a term t σ , by writing t I ν we mean either

I (t) (if t is a constant symbol) or ν(t) (if t is a variable).
A heap is a finite partial mapping h : L fin L k associating locations with k-tuples of locations. We denote by dom(h) the set of locations on which h is defined, by img(h) the set of locations occurring in the range of h, and by Heaps the set of heaps. Two heaps h 1 and h 2 are disjoint if dom(h 1 ) ∩ dom(h 2 ) = / 0. In this case, h 1 h 2 denotes their union, which is undefined if h 1 and h 2 are not disjoint. Given a valuation ν and a heap h, the semantics of SL formulae is defined as:

ν, h |= sl t 1 ≈ t 2 ⇔ (t 1 ) I ν = (t 2 ) I ν ν, h |= sl emp ⇔ h = / 0 ν, h |= sl x → (t 1 , . . . ,t k ) ⇔ h = { ν(x), ((t 1 ) I ν , . . . , (t k ) I ν ) } ν, h |= sl φ 1 * φ 2 ⇔ ∃h 1 , h 2 ∈ Heaps . h = h 1 h 2 and ν, h i |= sl φ i , i ∈ [2]
The semantics of boolean and first order connectives is the usual one, omitted for brevity. Given SL formulae φ and ψ, we say that φ entails ψ (i.e. φ |= sl ψ) iff ν, h |= sl φ implies ν, h |= sl ψ, for any valuation ν and heap h.

Inductive Systems of Predicates in Separation Logic

Let Pred be a countable set of predicates, each p σ 1 ...σ n ∈ Pred having an associated tuple of argument sorts. Given a tuple of terms (t σ 1 1 , . . . ,t σ n n ), we call p(t 1 , . . . ,t n ) a predicate atom. A predicate rule is a pair {φ(x, x 1 , . . . , x n ), q 1 (x 1 ), . . . , q n (x n )} , p(x) , where x, x 1 , . . . , x n are tuples whose corresponding sets of variables are pairwise disjoint, φ is a formula, called the constraint, p(x) is a predicate atom called the goal and q 1 (x 1 ), . . . , q n (x n ) are predicate atoms called subgoals. The variables x are the goal variables, whereas n i=1 x i are the subgoal variables.

An inductive system S (system, for short) is a finite set of predicate rules. In this paper, we consider inductive systems whose constraints belong to the SL fragment described in §2.1. We assume w.l.o.g. that each predicate p ∈ Pred is the goal of at least one rule of S and that there are no goals with the same predicate and different goal variables. We write p(x)

:= S R 1 | . . . | R m when { R 1 , p(x) , . . . , R m , p(x)
} is the set of all predicate rules in S with goal p(x). We consider only quantifier-free constraints, in which no disjunction occurs positively and no conjunction occurs negatively, and assume that the set of constraints of a system has a decidable satisfiability problem. Disjunctions can be eliminated by splitting {φ 1 ∨ . . . ∨ φ m , q 1 (x 1 ), . . . , q n (x n )}, p(x) into m rules {φ i , q 1 (x 1 ), . . . , q n (x n )} , p(x) , one for each i ∈ [m].

Example 1 Consider the SL inductive system S AB consisting of the predicate rules:

p(x) := S AB x → (x 1 , x 2 ), p 1 (x 1 ), p 2 (x 2 ) q(x) := S AB x → (x 1 , x 2 ), q 1 (x 1 ), q 2 (x 2 ) | x → (x 1 , x 2 ), q 2 (x 1 ), q 1 (x 2 ) p 1 (x) := S AB x → (x 1 , nil), p 1 (x 1 ) | x → (nil, x) q 1 (x) := S AB x → (x 1 , nil), q 1 (x 1 ) | x → (nil, x) p 2 (x) := S AB x → (x 1 , nil), p 2 (x 1 ) | x → (nil, nil) q 2 (x) := S AB x → (x 1 , nil), q 2 (x 1 ) | x → (nil, nil)
Broadly speaking, the predicates define binary trees in which the root node points to two lists and one leaf is not nil, but its position differs in each definition.

Given an SL inductive system S, an assignment X maps each predicate p σ 1 ...σ n ∈ Pred to a set X (p) ⊆ L n × Heaps. For a set F = {φ, q 1 (x 1 ), . . . , q n (x n )}, where φ is an SL formula and q 1 (x 1 ), . . . , q n (x n ) are predicate atoms, we define

X ( * F) = {(ν, h 0 m i=1 h i ) | ν, h 0 |= sl φ, (ν(x i ), h i ) ∈ X (q i ), ∀i ∈ [m]}.
Then S induces a function F sl S (X ) on assignments, which maps each predicate p ∈ Pred into the set

m i=1 {(ν(x), h) | (ν, h) ∈ X ( * R i )}, where p(x) := S R 1 | . . . | R m . A solution of S is an assignment X such that F sl S (X ) ⊆ X
, where inclusion between assignments is defined pointwise.

It can be shown that the set of all assignments, together with the ⊆ relation, is a complete lattice and that F I S is monotone. Therefore, by the Knaster-Tarski theorem,

µS sl = {X | F I S (X ) ⊆ X }
is the least fixed point of F sl S and the least solution of S.

Example 2 Considering the S AB inductive system from Example 1, the set µS sl AB (q) consists of trees of both following forms, where n ≥ 1 and m ≥ 1:

x x 1 1 . . . nil x 1 2 . . . nil x n 1 nil nil x n 1 x m 2 nil nil nil x x 1 1 . . . nil x 1 2 . . . nil x n 1 nil nil nil x m 2 nil nil x m 2
while the set µS sl AB (p) contains trees of the first above form, but not the second.

We are concerned with the following entailment problem: given an inductive system S and predicates p σ 1 ...σ m , q σ 1 ...σ m 1 , . . . , q σ 1 ...σ m n , is it true that µS sl (p) ⊆ n i=1 µS sl (q i )? We denote entailment problems as p |= sl S q 1 , . . . , q n .

Example 3 Given the least solution of the S AB inductive system from Example 2, observe that the entailment p |= sl S AB q holds, while q |= sl S AB p does not.

Tree Automata Inclusion as Cyclic Proof Search

We consider top-down nondeterministic finite tree automata (NFTA), where a tree over a ranked alphabet F is either a symbol a ∈ F of rank (or arity) 0, or f (t 1 , . . . ,t n ) such that f ∈ F is of rank n and t 1 , . . . ,t n are, in turn, trees. The actions of an NFTA are described by transition rules ECEASST q f -→ (q 1 , . . . , q n ), with the following meaning: if the automaton is in state q and the input is a tree f (t 1 , . . . ,t n ), then it moves simultaneously on each t i changing its state to q i , for all i ∈ [n]. A tree is accepted by an automaton A if each leaf can be eventually read by a transition of the form q a -→ (). The language of a state q in A, denoted L(A,q), is the set of trees accepted by A starting with state q.

An NFTA can be naturally viewed as an inductive system, where predicates represent states and predicate rules are obtained directly from transition rules. For instance, q f -→ (q 1 , . . . , q n ) can be written as {x ≈ f (x 1 , . . . , x n ), q 1 (x 1 ), . . . , q n (x n )}, q(x) , where variables range over trees and the function symbols are interpreted in the canonical (Herbrand) sense. To further obtain an SL inductive system, an encoding of the constraints in each predicate rule using SL connectives is required.

Example 4 The SL inductive system S AB from Example 1 encodes two NFTA A and B with states {p, p 1 , p 2 } and {q, q 1 , q 2 }, respectively, where p and q are initial states, using the alphabet { f (, ), g(), a, b} and having the transition sets

{p f → (p 1 , p 2 ), p 1 g → p 1 , p 1 a → (), p 2 g → p 2 , p 2 b → ()} and {q f → (q 1 , q 2 ), q f → (q 2 , q 1 ), q 1 g → q 1 , q 1 a → (), q 2 g → q 2 , q 2 b → ()},
respectively. We encoded the binary symbol f as x → (x 1 , x 2 ), the unary symbol g as x → (x 1 , nil), and the constant symbols a and b as x → (nil, x) and x → (nil, nil), respectively, where x, x 1 and x 2 are always allocated, thus different from nil.

Since language inclusion is decidable for NFTA [CDG + 05, Corollary 1.7.9], we leverage an existing algorithm for this problem by Holík et al. [START_REF] Holík | Efficient Inclusion Checking on Explicit and Semi-symbolic Tree Automata[END_REF] to build a set of inference rules and derive a proof search technique. This algorithm searches for counterexamples of the inclusion problem L(A, p) ⊆ n i=1 L(B,q i ) by enumerating pairs (r, {s 1 , . . . , s m }), where r is a state that can be reached via a series of transitions from p, and {s 1 , . . . , s m } are all the states that can be reached via the same series of transitions from q 1 , . . . , q k . A counterexample is found when reaching a pair (r, {s 1 , . . . , s m }) such that there exists a transition r f → (r 1 , . . . , r k ), but there is no transition

s i f → (s 1 i , . . . , s k i ) for any i ∈ [m].
Example 5 Consider the NFTA A and B from Example 4. To check L(A, p) ⊆ L(B,q), we start with (p, {q}). A possible run is:

(p, {q}) ((p 1 , p 2 ), {(q 1 , q 2 ), (q 2 , q 1 )}) (p 1 , {q 1 , q 2 }) (p 1 , {q 1 }) (p 2 , {q 2 }) (p 2 , {q 2 , q 1 }) ((), {()}) (p 1 , {q 1 , q 2 }) ((), {()}) (p 1 , {q 1 }) ((), {()}) (p 2 , {q 2 }) ((), {()}) (p 2 , {q 2 , q 1 }) f a g a g b g b g
The algorithm performs two types of moves: transitions and split actions. The arrows labeled by symbols f , g, a and b are transitions, for instance the arrow labeled by f takes p into the tuple (p 1 , p 2 ) by the transition p f -→ (p 1 , p 2 ) and {q} into the set of tuples {(q 1 , q 2 ), (q 2 , q 1 )}, by the transitions q f -→ (q 1 , q 2 ) and q f -→ (q 2 , q 1 ). However, the pair ((p 1 , p 2 ), {(q 1 , q 2 ), (q 2 , q 1 )})

is problematic because it asserts that L(A, p 1 ) × L(A, p 2 ) ⊆ L(B,q 1 ) × L(B,q 2 ) ∪ L(B,q 2 ) × L(B,q 1 ). Using several properties of the Cartesian product [HLSV11, Theorem 1] there are multiple ways to split this proof obligation into several simpler conjunctive subgoals. If at least one split move leads to a proof, then the inital proof obligation holds. The split move used above simultaneously considers (p 1 , {q 1 , q 2 }), (p 1 , {q 1 }), (p 2 , {q 2 }) and (p 2 , {q 2 , q 1 }), together asserting that L(A, p 1 ) ⊆ L(B,q 1 ) and L(A, p 2 ) ⊆ L(B,q 2 ). The other options are:

(1

) (p 1 , {q 1 , q 2 }) (p 1 , {q 1 }), (p 1 , {q 2 })
, and (p 2 , {q 2 , q 1 });

(2) (p 1 , {q 1 , q 2 }), (p 2 , {q 1 }), (p 1 , {q 2 }), and (p 2 , {q 2 , q 1 });

(3) (p 1 , {q 1 , q 2 }), (p 2 , {q 1 }), (p 2 , {q 2 }), and (p 2 , {q 2 , q 1 }).

The algorithm does not expand nodes (p, S) with p ∈ S, for which inclusion holds trivially, or having a predecessor (p, S ) with S ⊆ S (enclosed in dashed boxes), since any counterexample that can be found from (p, S) could have been discovered from (p, S ).

A Proof Search Semi-algorithm

(IR) Γ 1 ∆ 1 . . . Γ n ∆ n Γ ∆ side conditions . . . . C Γ p ∆ p
We denote sequents as Γ ∆, where Γ and ∆ are sets of formulae and commas are read as set union, thus contraction rules are not necessary. We omit braces and a sequent of the form p(x) q 1 (x), . . . , q n (x) is called basic. An inference rule schema IR is a possibly infinite set of inference rules, called instances of the schema, sharing the same pattern. An inference rule has antecedents Γ 1 ∆ 1 , . . . , Γ n ∆ n , and a consequent Γ ∆. We write for an empty antecedent list and an inference rule without antecedents may have a pivot Γ p ∆ p , which is an ancestor of the consequent or, in other words, a sequent preceding the consequent in the transitive closure of the consequent-antecedent relation. The sequence of inference rules applied along the path between the pivot and the consequent is subject to a pivot condition C.

A proof system is a set R of inference rule schemata. A derivation built with R is a possibly infinite tree D = (V, v 0 , S, R, P, B), where V is a set of vertices (or nodes) and v 0 ∈ V is the root. Every v ∈ V is labeled with sequent S(v) and an inference rule schema

R(v) ∈ R such that S(v) is the consequent of the instance of R(v) applied at v. Moreover, B(v) ∈ V is a node such that S(B(v)) is the pivot for R(v), if it has one. We call (v, B(v)) a backlink. If v = v 0 , P(v)
is the parent of v in the derivation and S(v) is an antecedent for the instance of R(P(v)) with consequent S(P(v)). A proof is a finite derivation in which S(v) = for all leaves v ∈ V -i.e. on every branch of the derivation, the last inference rule application generates an empty list of antecedents. Given an inductive system S and predicates p σ 1 ,...,σ n , q σ 1 ,...,σ n 1 , . . ., q σ 1 ,...,σ n k ∈ Pred, a proof system R is: (i) sound if, for any proof D = (V, v 0 , S, R, P, B) with S(v 0 ) = p(x) q 1 (x), . . . , q n (x), we have p |= sl S q 1 , . . . , q n , (ii) complete if p |= sl S q 1 , . . . , q n implies the existence of a proof D = (V, v 0 , S, R, P, B) with S(v 0 ) = p(x) q 1 (x), . . . , q n (x).

A sequence π = v 1 , . . . , v n of vertices is a trace if, for any i ∈ [n -1], either v i = P(v i+1 ) or v i+1 = B(v i ).
π is path if only the former condition holds and, moreover, a direct path if v 1 = B(v n ). We denote by Λ(π) = R(v 1 ), . . . , R(v n -1) the sequence of inference rule schemata ECEASST applied between v 1 and v n . An inference rule schema IR is applicable on v n and π if there exists an instance ir of IR whose consequent matches S(v n ) and whose pivot (if it exists) matches S(v i ) for some i < n, such that both the side conditions of ir are satisfied and and Λ(v i , . . . , v n ) abides by its pivot condition. A strategy is a set S of inference rule schemata sequences. A sequence s is a valid prefix for S if there exists another sequence s such that their concatenation s

• s ∈ S. A derivation (proof) D is an S-derivation (S-proof) if, for each maximal path π in D, Λ(π) ∈ S.
Algorithm 1 Proof search semi-algorithm.

data structure: Node(sequent, rule, parent, pivot, children), where:

• sequent is the sequent that labels the node,

• rule is the inference rule with consequent sequent.

• parent is the link to the parent of the node,

• pivot is the pivot for the instance of rule applied on sequent • children is the list of children nodes input: inductive system S, sequent p(x) q 1 (x), . . . , q n (x), proof system R , strategy S output: an S-proof built with R , whose root is labeled with sequent p(x) q 1 (x), . . . , q n (x)

1: Root ← Node(p(x) q 1 (x), . . . , q n (x), null, null, null, []) 2: WorkList ← {Root} 3: while WorkList = / 0 do 4:
remove N from WorkList if N not Closed and Λ(π) • IR is a valid prefix of S for some IR ∈ R N then 14:

let ir be an instance of IR such that N.sequent is the consequent of ir 15:

for each antecedent Γ ∆ of ir do 16:

N ← Node(Γ ∆ , null, N, null, []) 17:
add N to N.children and to WorkList 18:

if N.children is empty then mark N as Closed Given an input sequent p(x) q 1 (x), . . . , q n (x), a set R of inference rules and a strategy S, the proof search semi-algorithm 1 uses a worklist iteration to build a derivation of p(x) q 1 (x), . . . , q n (x). When a node is removed from the worklist, it chooses (non-deterministically) an inference rule and an instance whose consequent matches the sequent of the node, if one exists. To speed up termination, inference rule schemata without antecedents are considered eagerly (line 8). If a proof of the input sequent exists, then there exists a finite execution of the semi-algorithm 1 leading to it.

(LU) R i (x, y i ), Γ \ p(x) ∆ n i=1 Γ ∆ p(x)∈Γ, p(x):= S R 1 (x,y 1 )|...|R n (x,y n ) y 1 ,...,y n fresh variables (RU) Γ {∃y i . * R i (x, y i )} n i=1 , ∆ \ p(x) Γ ∆ p(x)∈∆, y 1 ,...,y n fresh p(x):= S R 1 (x,y 1 )|...|R n (x,y n ) (RD) p 1 (x 1 ), . . . , p n (x n ) {Q j θ | θ ∈ S j } i j=1 φ(x, x 1 , . . . , x n ), p 1 (x 1 ), . . . , p n (x n ) {∃y j . ψ j (x, y j ) * Q j (y j )} k j=1 φ|= sl i j=1 ∃y j .ψ j φ |= sl k j=i+1 ∃y j .ψ j S j ⊆Sk(φ,ψ j ), j∈[i] (AX) Γ ∆ * Γ|= sl ∆ (ID) Γθ ∆ θ θ flat injective substitution ∆ ⊆ ∆ . . . . (R sl Ind ) * •LU•(R sl Ind ) * Γ ∆ (SP) p ī j (x) {q ī j (x) | ∈ [k], f j (Q ) = ī j } n k j=1 p 1 (x 1 ), . . . , p n (x n ) Q 1 (x 1 , . . . , x n ), . . . , Q k (x 1 , . . . , x n ) ∀i, j∈[n] . x i ∩x j = / 0, ī∈[n] n k Q i = * n j=1 q i j (x j ),Q i = q i 1 ,...,q i n F (Q 1 ,...,Q k )={ f 1 ,..., f n k } Figure 1: The set R sl
Ind of inference rule schemata for inductive entailments in SL.

(RD) eliminates constraints from both sides of a sequent. The existentially quantified variables on the right-hand side are replaced using a (subset of) the finite set Sk(φ, ψ j ) = {θ : k i=1 y i → {nil} ∪ x ∪ n i=1 x i ) | φ |= sl ψ j θ} of substitutions that witness the entailments φ(x, x 1 , . . . , x n ) |= sl ∃y j . ψ j between the left and right constraints.

A transition move in the language inclusion algorithm of [START_REF] Holík | Efficient Inclusion Checking on Explicit and Semi-symbolic Tree Automata[END_REF] (Example 5) performs (LU), (RU) and (RD) all at once. This is natural because the transition rules of tree automata are controlled uniquely by the function symbols labeling the root of the current input tree, which can be matched unambiguously. When considering more general constraints, matching amounts to discovering non-trivial substitutions that prove an entailment between existentially quantified constraints.

(SP) generalizes the split moves performed by the language inclusion algorithm of [START_REF] Holík | Efficient Inclusion Checking on Explicit and Semi-symbolic Tree Automata[END_REF] and breaks a sequent p 1 (x 1 ), . . . ,

p n (x n ) Q 1 (x 1 , . . . , x n ), . . . , Q n (x 1 , . . . , x n ) into basic sequents. Given tuples {Q 1 , . . . , Q k } ⊆ Pred n with n ≥ 1, a choice function f maps each tuple Q i into an index f (Q i ) ∈ [n]
corresponding to a position in the tuple. Let F (Q 1 , . . . , Q k ) be the set of such choice functions, having cardinality n k ≤ n ||Pred|| n . Given a tuple ī ∈ [n] n k , associating a value in

[n] to each choice function f ∈ F (Q 1 , . . . , Q k ),
there exists an application of (SP) generating n k antecedents with left hand-side p ī j (x ī j ), j ∈ [n k ] and right hand-side consisting of all predicate ECEASST atoms q ī j (x ī j ), ∈ [k] obtained from predicates at position ī j in the tuples Q which are mapped to ī j by the choice function f j . In order to obtain a proof, there must exist some application of (SP) -and, therefore, some ī ∈ [n] n k -for which all the generated antecedents can be proven.

As shown in [HLSV11, Section 3], the tuples ī ∈ [n] n k encode the transformation of a formula from CNF to DNF and, as such, not all are relevant. More precisely, any ī for which there exists j ∈ [n k ] such that ī j ∈ img( f j ) can be discarded.

(AX) closes the current branch of the proof if the sequent can be proved using a decision procedure for the underlying constraint logic, by treating predicate symbols as uninterpreted boolean functions. This is a generalization of encountering a pair (p, S) with p ∈ S in the NFTA language inclusion algorithm of [START_REF] Holík | Efficient Inclusion Checking on Explicit and Semi-symbolic Tree Automata[END_REF].

(ID) introduces backlinks in a derivation, from the consequent Γθ ∆ θ to a pivot Γ ∆. The pivot condition (R sl Ind ) * • LU • (R sl Ind ) * requires that (LU) must be applied on the direct path between the pivot and the consequent. Observe that, if Γθ ∆ θ denotes a non-valid entailment, there exists (ν, h) ∈ µS sl ( * Γθ) \ µS sl ( ∆ θ). Since θ is surjective by construction and injective by the side condition, the restriction of θ to FV(Γ ∪ ∆ ) has an inverse and, because ∆ ⊆ ∆, we obtain that (ν • θ -1 , h) ∈ µS sl ( * Γ) \ µS sl ( ∆) is a counterexample for the pivot.

The local soundness of R sl Ind \ {ID} is given by [IS17, Lemma 15], whereas the soundness of proofs containing (ID) is established by [IS17, Theorem 6] through the following argument. If the root sequent of a proof denotes an entailment that admits a counterexample, then, by the local soundness, there exists a path in the proof on which this counterexample can be propagated. This path may not end with an application of (AX), as it would violate its side condition, and, thus, must end with an application of (ID), which allows it to be extended to an infinite trace. Then, using the reasoning above to additionally propagate counterexamples through a backlinks, we obtain that the counterexample for the root sequent can also be propagated along a trace with an infinite number of direct paths [IS17, Proposition 1]. We use an additional ranking assumption given by a pre-established well-founded ordering of the counterexamples. In SL, we consider the subheap ordering, where h 1 ¢ h 2 iff there exists h ∈ Heaps such that h 2 = h 1 h and h 1 ¡ h 2 if, moreover, h = / 0. An SL inductive system is ranked if the constraints of every predicate rule with at least one subgoal do not admit an empty heap model. Since (LU) is required on each direct path, this leads to an infinite sequence of counterexamples (ν 1 , h 1 ), (ν 2 , h 2 ), . . . with strictly decreasing heaps h 1 £ h 2 £ . . . (see [IS17, Lemma 15] and the proof of [IS17, Theorem 6]). However, since the subheap ordering is well-founded, the existence of such sequences is prohibited. We have reached a contradiction and may conclude that there was no counterexample to begin with.

Analogously, the language inclusion algorithm of [START_REF] Holík | Efficient Inclusion Checking on Explicit and Semi-symbolic Tree Automata[END_REF] stops expanding a branch in the search tree whenever it has discovered a pair (p, S) that has a predecessor (p, S ), with S ⊆ S. Just as for the (ID) inference rules, backtracking relies on the Infinite Descent principle [START_REF] Bussey | Fermat's Method of Infinite Descent[END_REF], that forbids infinitely descending sequences of counterexamples.

Example 6 Given the system S AB from Example 1, we can use R sl Ind to build a proof for p(x) q(x), partially shown below -we only include the subproof for the first sequent obtained after split. Note the similarities with the proof tree in Example 5.

p 1 (x) q 1 (x), q 2 (x)
x → (nil, x) q 1 (x), q 2 (x)

x → (nil, x) x → (nil, x), q 2 (x), ∃y 1 . x → (y 1 , nil) * q 1 (y 1 )

x → (x 1 , nil), p 1 (x 1 ) q 1 (x), q 2 (x)

x → (x 1 , nil), p 1 (x 1 ) x → (nil, x), ∃y 1 . x → (y 1 , nil) * q 1 (y 1 ), q 2 (x)

x → (x 1 , nil), p 1 (x 1 ) x → (nil, x), ∃y 1 . x → (y 1 , nil) * q 1 (y 1 ), x → (nil, nil), ∃y 1 . x → (y 1 , nil) * q 2 (y 1 ) p 1 (x) q 1 (x), q 2 (x)

LU RU AX RU RU RD ID p(x) q(x)
x → (x 1 , x 2 ), p 1 (x 1 ), p 2 (x 2 ) q(x)

x → (x 1 , x 2 ), p 1 (x 1 ), p 2 (x 2 ) ∃y 1 , y 2 . x → (y 1 , y 2 ) * q 1 (y 1 ) * q 2 (y 2 ), ∃y 1 , y 2 . x → (y 1 , y 2 ) * q 2 (y 1 ) * q 1 (y 2 )

p 1 (x 1 ), p 2 (x 2 ) q 1 (x 1 ) * q 2 (x 2 ), q 2 (x 1 ) * q 1 (x 2 ) p 1 (x) q 1 (x), q 2 (x) p 1 (x) q 1 (x) p 2 (x) q 2 (x) p 2 (x) q 2 (x), q 1 (x) LU RU RD SP
For (SP), let Q 1 = (q 1 , q 2 ) and Q 2 = (q 2 , q 1 ) be the tuples of predicates on the right-hand side. set of choice functions is

F (Q 1 , Q 2 ) = { f 1 = {(Q 1 , 1), (Q 2 , 1)}, f 2 = {(Q 1 , 1), (Q 2 , 2)}, f 3 = {(Q 1 , 2), (Q 2 , 1)}, f 4 = {(Q 1 , 2), (Q 2 , 2)}}. Out of the 16 index choice tuples for F (Q 1 , Q 2 ), only (1, 1, 1, 2), (1, 1, 2, 2), (1, 2, 1, 2)
and (1, 2, 2, 2) are relevant. To obtain the above proof, we chose ī = (1, 1, 2, 2).

Only the ranking assumption is necessary to ensure soundness of R sl Ind . Three additional restrictions required for completeness are given in [IS17, Section 4.2]. Effectively checking whether a given inductive system satisfies these restrictions requires the existence of a decision procedure for the ∃ * ∀ * -quantified fragment of the underlying logic. In general, this problem is undecidable for SL [EIP18, Theorem 1], but the fragment decribed in §2.1 omits the -- * operator (primarily responsible for loss of decidability), while the → operator only maps elements in L to tuples in L k . As such, the satisfiability of ∃ * ∀ * -quantified formulae is PSPACE-complete in the fragment we consider [EIP18, Theorems 2 and 3]. A suitable decision procedure for this fragment of SL is given in [START_REF] Reynolds | Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic[END_REF]. Completeness is then assured for entailments involving inductive definitions which generate matching coverage trees of the heap (see [IS17, Section 4.3]).

Example 7 Consider the following definitions for doubly-linked lists: dlls(hd, p,tl, n

) := S hd ≈ tl ∧ hd → (p, n) | hd → (p, x), dlls(x, hd,tl, n) dlls r (hd, p,tl, n) := S hd ≈ tl ∧ hd → (p, n)
| tl → (n,tl ), dlls r (hd, p, x,tl)

t 1 = {(1, 0, 2 )} {(2, 1, 3 )} {(3, 2, 4 )} t 2 = {(3, 2, 4 )} {(2, 1, 3 )} {(1, 0, 2 )}
The predicate dlls unfolds the list starting at the head, while dlls r unfolds it starting at the tail. Both dlls |= sl S dlls r and dlls r |= sl S dlls hold, but they cannot be proven using our inference rules. Take, for instance, the tuple = 0, 1, 3, 4 and the heap h = {(1, 0, 2 ), (2, 1, 3 ), (3, 2, 4 )}. The pair ( , h) belongs to both µS sl (dlls) and µS sl (dlls r ), but dlls generates the coverage tree t 1 for h, while dlls r generates the coverage tree t 2 . Since the trees do not match, R sl ECEASST 3 An Inductive Entailment Checker for Separation Logic

In this section we describe Inductor, an entailment checker tool that implements the proof-search semi-algorithm 1 from §2.4, using the set R sl Ind of inference rules for inductive entailments in SL. Inductor is written in C++ and uses the DPLL(T )-based SMT solver CVC4 [BCD + 11] as a backend that it queries in order to establish the satisfiability of SL formulae, in which the occurrences of inductive predicates are treated as uninterpreted functions. More specifically, these queries are handled by the decision procedures provided in [START_REF] Reynolds | A Decision Procedure for Separation Logic in SMT[END_REF][START_REF] Reynolds | Reasoning in the Bernays-Schönfinkel-Ramsey Fragment of Separation Logic[END_REF] and integrated into CVC4.

The inputs mainly handled by Inductor are SMT-LIB scripts, abiding by the SMT-LIB Standard: Version 2.6 [START_REF] Barrett | The SMT-LIB Standard: Version 2[END_REF]. Theory and logic files are loaded automatically, based on the logic set in the input script being handled. Additionally, proof strategies are specified as nondeterministic finite word automata (NFA), in a language similar to that accepted by libVATA [LSV + ] (for more details, see Appendix B.1). The front-end interprets these input files using custom parsers constructed with Flex 1 and Bison 2 .

A Breadth-First Proof Search Implementation

The proof search method sketched by algorithm 1 is reliant on the choice of IR made at lines 8 and 13. Whenever there are more than one applicable inference rules, only one is selected and the rest are discarded. Furthermore, as is the case for SP, some inference rules can have multiple possible instances for the same sequent, where only one is required to succeed in obtaining a proof. Algorithm 1 again only chooses one of them. In our implementation, we wanted to explore all the potential derivations resulting from the inference rule instances available at any point. Moreover, since we use a queue for the nodes still needing to be explored, we generate derivations in a breadth-first fashion. Thus, proofs or counterexample are obtained from the shortest possible paths.

We use a different tree-like structure to compactly store all the derivations explored. This structure accepts two types of nodes, depicted in Figure 2, which represent sequents (SNode) and inference rule instances (RNode), respectively. The node types alternate in the tree, thus an SNode only has RNode children, and vice-versa. With these new data structures, we say that an inference rule IR ∈ R sl Ind is applicable on a given SNode N whenever there exists an instance ir of IR for which: (i) the consequent of ir matches N.sequent and the pivot of ir matches N .sequent, for some SNode ancestor N of N, such that the side conditions of ir are satisfied, and (ii) if R 1 , . . . , R n is the RNode sequence extracted from 1 Flex -The Fast Lexical Analyzer, github.com/westes/flex 2 GNU Bison -The Yacc-compatible Parser Generator, www.gnu.org/software/bison the path starting at N and ending at N, then the sequence R 1 .rule, . . . , R n .rule satisfies the pivot condition of ir.

Algorithm 2 Sketch of our exhaustive proof search implementation input: an SL inductive system S, a basic sequent p(x) q 1 (x), . . . , q n (x), and a proof strategy NFA S = (Q S , R sl Ind , T S , q 0 , F S )

output: VALID and an S-proof starting with p(x) q 1 (x), . . . , q n (x), built with R sl Ind ; INVALID and a counterexample for p(x) q 1 (x), . . . , q n (x); UNKNOWN and the proof search tree constructed by the algorithm

1: Root ← SNode(p(x) q 1 (x), . . . , q n (x), [q 0 ], null, []) 2: Queue ← {Root} 3: while Queue = [] and Root is Unknown do 4: dequeue N from Queue 5: let Q IR N = {q | (q, IR) → q ∈ T S and q ∈ N.states} for any IR ∈ R sl Ind 6: let R N = {IR | Q IR N = / 0 and IR applicable on N} 7: if AX ∈ R N and Q AX N ∩ F S = / 0 then 8:
R ← RNode(AX, null, N, []) and add R to N.children for each antecedent

9: N ← SNode( , Q AX N , R, []), add N to R.
Γ i ∆ i of ir with i ∈ [k] do 20: N i ← SNode(Γ i ∆ i , Q IR N , R, []) and add N i to R.children 21: if ∆ i = / 0 then mark N i as Failed 22: if R is not Failed then enqueue N 1 , . . . , N k in Queue 23: if Root is Closed then 24:
return VALID and ExtractProof(Root) 25: else if Root is Failed then 26:

return INVALID and ExtractCounterexamples(Root) 27: else return UNKNOWN and Root Both types of nodes are marked with either a Closed, Failed or Unknown status. All nodes are initially Unknown. The status of an SNode can be changed to Closed whenever: (i) its sequent is , or (ii) at least one of its RNode children is Closed. An RNode becomes Closed when all of its SNode children are Closed. Conversely, an SNode is marked as Failed whenever: (i) its sequent is of the form Γ / 0, or (ii) all of its RNode children are Failed. An RNode is marked Failed when at least one of its SNode children is Failed. Changing the status of a node prompts tree + 2 (x) tree + 1 (x)

x → (l 0 , r 0 ), tree + 2 (l 0 ), tree + 2 (r 0 ) tree + 1 (x)

x → (l 0 , r 0 ), tree + 2 (l 0 ), tree + 2 (r 0 ) x → (nil, nil), ∃l 1 ∃r 1 . x → (l 1 , r 1 ) * tree + 1 (l 1 ) * tree(r 1 ), ∃l 1 ∃r 1 . x → (l 1 , r 1 ) * tree(l 1 ) * tree + 1 (r 1 ) tree + 2 (l 0 ), tree + 2 (r 0 ) tree + 1 (l 0 ) * tree(r 0 ), tree(l 0 ) * tree + 1 (r 0 ) tree + 2 (l 0 ) tree(l 0 ) l 0 → (l 00 , r 00 ), tree + 2 (l 00 ), tree + 2 (r 00 ) tree(l 0 ) l 0 → (l 00 , r 00 ), tree + 2 (l 00 ), tree + 2 (r 00 ) l 0 → (nil, nil), ∃l 11 ∃r 11 . l 0 → (l 11 , r 11 ) * tree(l 11 ) * tree(r 11 ) tree + 2 (l 00 ), tree + 2 (r 00 ) tree(l 00 ) * tree(r 00 ) tree + 2 (l 00 ) tree(l 00 )

Case Study: Possibly Cyclic and Acyclic List Segments

Consider the following ranked definitions for possibly cyclic and acyclic list segments.

ls(x, y)

:= S l x ≈ y ∧ emp | x → z, ls(z, y) ls a (x, y) := S l x ≈ y ∧ emp | ¬(x ≈ y) ∧ x → z, ls a (z, y)
Naturally, the entailment ls a |= sl S l ls holds, while ls |= sl S l ls a does not. The proof for the former case is shown below. In the latter case, the counterexample provided by Inductor for ls(x, y) ls a (x, y) is x ≈ y∧x → z 0 * ls(z 0 , y), from which we can obtain the more concrete one x ≈ y∧x → z 0 * (z 0 ≈ y ∧ emp), further simplified to x → x. ls a (x, y) ls(x, y)

x ≈ y ∧ emp ls(x, y)

x ≈ y ∧ emp x ≈ y ∧ emp, ls(x, y) ¬(x ≈ y) ∧ x → z 0 , ls a (z 0 , y) ls(x, y) ¬(x ≈ y) ∧ x → z 0 , ls a (z 0 , y) x ≈ y ∧ emp, ∃z 1 .x → z 1 * ls(z 1 , y) ls a (z 0 , y) ls(z 1 , y) We adapt our definitions from §3.3 to a fragment in which each memory location points to a pair of locations, and use them to define lists whose elements point at possibly cyclic or acyclic list segments. The last elements of these list segments are, in turn, linked backwards and the last element of the primary list points to the last element of the last secondary list segment. The entailment lls a |= sl S ll lls holds, while its reverse lls |= sl S ll lls a does not. Part of the proof for lls a (x, v) lls(x, v) is shown below. The subproof for ls a (u 0 , v) ls(u 0 , v) is mostly skipped as it is identical to the one from §3.3 modulo a variable renaming. lls a (x, v) lls(x, v)

x → (z 0 , u 0 ) * w 0 → (v, nil), ls a (u 0 , v), lls a (z 0 , w 0 ) lls(x, v)

x → (z 0 , u 0 ) * w 0 → (v, nil), ls a (u 0 , v), lls a (z 0 , w 0 ) x ≈ nil ∧ emp,

∃z 1 ∃u 1 ∃w 1 . x → (z 1 , u 1 ) * w 1 → (v, nil) * ls(u 1 , v) * lls(z 1 , w 1 )
ls a (u 0 , v), lls a (z 0 , w 0 ) ls(u 0 , v) * lls(z 0 , w 0 ) ls a (u 0 , v) ls(u 0 , v)

. . . The counterexample provided by Inductor for lls(x, v) lls a (x, v) is x → (z 0 , u 0 ) * w 0 → (v, nil) * (u 0 ≈ v ∧ u 0 → (u 00 , nil) * ls(u 00 , v)) * lls(z 0 , w 0 ), from which we obtain the more concrete one

x → (z 0 , u 0 ) * w 0 → (v, nil) * (u 0 ≈ v ∧ u 0 → (u 00 , nil) * (u 00 ≈ v ∧ emp)) * (z 0 ≈ w 0 ∧ emp), further simplified to x → (z 0 , v) * z 0 → (v, nil) * v → (v, nil).

Experimental results

Table 1 summarizes the experimental results obtained for the entailments discussed in §3.2-3.5. All experiments were run on a 2.10GHz Intel R Core TM i7-4600U CPU machine with 4MB of cache. For each case, we indicate: (i) the result (column R), which can be V for VALID or I for INVALID, (ii) the total number of sequent nodes (column Seq), the maximum number of sequent nodes along a branch (column H) and the maximum number of (LU) and (SP) applications along a branch (columns H LU and H SP ) of the tree structure defined in Figure 2, which encodes the derivation, (iii) the run time for the proof search algorithm (column T), and (iv) the total number of calls to CVC4 (column CVC4). As shown by the T column in both halves of the table, the execution times are fairly low. The size of the derivations is influenced by how elaborate the inductive definitions are. For instance, tree + 1 is defined by three predicate rules, thus when encountered on the left-hand side of an entailment will generate a larger number of nodes due to left-unfolding. On the right-hand side, the number of predicate rules in a definition and the number of subgoals in each predicate rule both influence the complexity of (SP), which can lead to higher execution times than expected, given the size of the derivation, since all instances of (SP) need to be generated and then checked.

Conclusions

We describe an entailment checker tool called Inductor, which implements a cyclic proof system for Separation Logic with inductive definitions and utilizes dedicated decision procedures in the SMT solver CVC4 to establish the satisfiability of quantifier-free or ∃ * ∀ * -quantified Separation Logic formulae. The tool outputs a proof whenever an entailment is found to be valid, or counterexamples when it is not. Soundness is warranted by imposing a ranking restriction on the inductive system given as input. It is possible, although the results may be inconclusive, to use Inductor outside of these boundaries. We discuss several case studies and provide experimental results showing fairly low execution times and moderate sizes for the derivations built by the tool in order to obtain proofs or counterexamples.

Our inference rules build cyclic proofs with backlinks in similar fashion as CYCLIST [START_REF] Brotherston | A Generic Cyclic Theorem Prover[END_REF],

ECEASST closing recurring branches of a proof with (ID). We restrict backlinks to ancestral nodes, which allows us to embed the condition necessary to ensure progress along an infinite trace directly into (ID). Because we allow disjunctions on the right-hand side of sequents and (RU) introduces all the cases of an inductive definition -as opposed to CYCLIST and [START_REF] Chu | Automatic Induction Proofs of Data-Structures in Imperative Programs[END_REF], which always choose only one -Inductor can tackle entailments such as ls + (x, y) |= sl S eo ls + (x, y) in §3.4, which CYCLIST and [CJT15] cannot prove. However, the cut rule in [START_REF] Chu | Automatic Induction Proofs of Data-Structures in Imperative Programs[END_REF] and the canonical rotation relation between trees in SLIDE [START_REF] Iosif | Deciding Entailments in Inductive Separation Logic with Tree Automata[END_REF] enable these systems to show entailments such as the ones in Example 7, for which Inductor cannot build proofs. On a different note, the fragment of inductive definitions that SLIDE can translate to tree automata does not allow disequalities between variables, thus it cannot handle predicates and entailments such as ls a (x, y) |= sl S l ls(x, y) in §3.3.

SLEEK [START_REF] Chin | Automated Verification of Shape, Size and Bag Properties via User-defined Predicates in Separation Logic[END_REF] and SPEN [ELS17, ESW15] go further than Inductor and are able to check much more complex verification conditions, involving, for instance, concatenations of predicates, formulae equivalent to several unfoldings of a predicate and various combinations of allocated heap cells and predicate calls. Although most of the inductive definitions for data structures used in these entailments fall into the fragment accepted by Inductor, the entailments themselves are out of the scope of our current implementation. Multiple extensions of the inference rules are possible in order to allow the building of proofs for such entailments (e.g. right unfolding inside the same formula multiple times, reducing any subset of constraints) and are considered for future work. • Page 4, first paragraph of Section 2.3 -Added a short explanation for what a tree is;

• Page 6, second paragraph of Section 2.4 -Changed "a sequent preceding the consequent [...]" to "an ancestor of the consequent or, in other words, a sequent preceding the consequent [...]" so it is more clear what we are referring to. Also changed "the antecedent list of each terminal (leaf) node is necessarily empty" to "S(v) = for all leaves v ∈ V -i.e. on every branch of the derivation, the last inference rule application generates an empty list of antecedents" for more clarity;

• Page 7, second line -Added the "(if it exists)" mention when referring to the pivot of an inference rule;

• Page 10 -Added Example 7 to better explain the incompleteness of our approach;

• Page 13, second counterexample for the case study in Section 3.2 -The entailment was initially reversed by mistake, corrected it to tree + 1 (x) tree + 2 (x);

• Sections 3.3 and 3.5 -Added "Possibly Cyclic" to both titles and used this phrase when referring to the ls predicate because it more clearly captures its inductive definition;

• Page 16, table with experimental results -As suggested by the reviewers, we added new columns to the table to convey more information, such as the maximum number of LU and SP applications on a branch and the number of calls to CVC4. We reran the experiments. Due to some changes in the code after submitting the first version of the paper, some results differ from the original ones;

• Conclusions -Added two paragraphs of discussion and comparison to related work.

B Additional Material B.1 Specifying Proof Strategies as Automata

Inductor can also accept a proof strategy as input -if no proof strategy is given, then S = (LU • RU * • RD • SP?) * • LU? • RU * • (AX | ID) from [IS17, Theorem 7] will be used as default. By Kleene's Theorem, it is known that, given a regular expression, there exists an equivalent nondeterministic finite word automaton (NFA), possibly with ε-transitions (NFA-ε). Figure 3 depicts a straightforward NFA-ε that is equivalent to S.

We are more interested in such a representation because, after applying a certain inference rule, we want to easily check which inference rules that comply with the strategy could be applied next. However, given an NFA-ε, the ε-transitions are cumbersome and, thus, we prefer an AVoCS 2018 20 / 21 ECEASST q 0 start q 1 q 2 q 3 q 4 q 5 equivalent NFA -which is guaranteed to exist, since the two classes of automata are known to be equivalent. As such, the proof strategies that Inductor accepts as input are given as NFA, rather than regular expressions. The definition of such an NFA is specified in a language inspired by the simplicity of the one used by libVATA [LSV + ] and whose grammar is depicted in Listing 1. Listing 1: Grammar for files specifying proof strategies as NFA Using this language, Listing 2 defines an NFA that is equivalent with the NFA-ε from Figure 3, and consequently, is also equivalent with our default proof search strategy.

Rules LU RU RD SP ID AX Automaton Default States q0 q1 q2 q3 q4 q5 Initial state q0

Final states q5 Transitions (q0, LU) -> q1 (q1, RD) -> q3 (q2, RI) -> q3 (q3, LU) -> q4 (q0, LU) -> q4 (q1, RD) -> q4 (q2, RI) -> q4 (q3, RU) -> q4 (q0, RU) -> q4 (q2, LU) -> q1 (q2, SP) -> q0 (q3, AX) -> q5 (q0, AX) -> q5 (q2, LU) -> q4 (q2, SP) -> q3 (q3, ID) -> q5 (q0, ID) -> q5 (q2, RU) -> q4 (q2, SP) -> q4 (q4, RU) -> q4 (q1, RU) -> q1 (q2, RI) -> q0 (q2, AX) -> q5 (q4, AX) -> q5 (q1, RD) -> q0 (q2, RI) -> q2 (q2, ID) -> q5 (q4, ID) -> q5 (q1, RD) -> q2

Listing 2: The definition of the NFA corresponding to the default proof search strategy

  the path between Root and N 6: let R N ⊆ R be the inference rule schemata applicable on N and π 7: let R 0 N ⊆ R N be the subset of R N with empty antecedent lists 8: if Λ(π) • IR is a valid prefix of S for some IR ∈ R 0 N then 9: let ir be an instance of IR such that N.sequent is the consequent of ir 10: N.rule ← IR 11: if ir has pivot N .sequent for some N ∈ π then N.pivot ← N 12: mark N as Closed 13:

2. 5

 5 The Set R sl Ind of Inference Rules for Separation Logic Entailments Figure1gives a set R sl Ind of inference rule schemata for the entailment problem in SL, which generalize the transitions and split actions performed by the NFTA language inclusion algorithm described in §2.3. To shorten the presentation, we writeΓ i ∆ i n i=1 for Γ 1 ∆ 1 , . . . , Γ n ∆ n .(LU) and (RU) unfold a predicate atom p(x) by replacing it with the set of predicate rules p(x) := S R 1 (x) | . . . | R n (x), with goal variables x and fresh subgoal variables. The left unfolding yields a set of sequents, one for each R i (x) with i ∈ [n], that must be all proved, whereas the right unfolding replaces p(x) with the set of formulae obtained from R 1 (x) | . . . | R n (x) in which the subgoal variables are existentially quantified.

SNodeFigure 2 :

 2 Figure 2: The data structures representing sequents and inference rule instances

  children and mark it as Closed 10: else if ID ∈ R N and Q ID N ∩ F S = / 0 then 11: R ← RNode(ID, N , N, []) for some pivot N of ID and add R to N.children 12: N ← SNode( , Q ID N , R, []), add N to R.children and mark it as Closed 13: else 14: for each instance ir of each IR ∈ R N do 15: R ← RNode(IR, null, N, []) and add R to N.children 16: let k be the number of antecedents generated by ir 17: if k = 0 and Q IR N ∩ F S = / 0 then 18: N ← SNode( , Q IR N , R, []), add N to R.children and mark it as Closed 19:

  Study: List Segments of Even and Odd LengthConsider the following ranked definitions for list segments of even and odd length, together with two alternate definitions of list segments with at least one element.ls e (x, y) ← S eo x ≈ y ∧ emp | x → z, ls o (z, y) ls o (x, y) ← S eo x → y | x → z, ls e (z,y) ls + (x, y) ← S eo x → y | x → z, ls + (z, y) ls + (x, y) ← S eo x → z, ls e (z, y) | x → z, ls o (z, y)

+

  (x, y) is shown below. For the invalid entailments, Inductor gives the counterexamples: x ≈ y ∧ emp for both ls e (x, y) ls + (x, y) and ls e (x, y) ls o (x, y); x → y for ls + (x, y) ls e (x, y); x → z 0 * z 0 → y for ls + (x, y) ls o (x, y).

  ECEASST ls + (x, y) ls + (x, y)x → z 0 , ls + (z 0 , y) ls+ (x, y) x → z 0 , ls + (z 0 , y) ∃z 1 . x → z 1 * ls e (z 1 , y), ∃z 1 . x → z 1 * ls o (z 1 , y)ls + (z 0 , y) ls e (z 0 , y), ls o (z 0 , y) z 0 → z 00 , ls + (z 00 , y) ls e (z 0 , y), ls o (z 0 , y) z 0 → z 00 , ls + (z 00 , y) z 0 ≈ y ∧ emp, ∃z 01 . z 0 → z 01 * ls o (z 01 , y), ls o (z 0 , y) z 0 → z 00 , ls + (z 00 , y) z 0 ≈ y ∧ emp, ∃z 01 . z 0 → z 01 * ls o (z 01 , y), z 0 → y, ∃z 11 . z 0 → z 11 * ls e (z 11 , y) ls + (z 00 , y) ls o (z 00 , y), ls e (z 00 , y) Study: Lists of Possibly Cyclic and Acyclic List Segments

  ls(x, y) := S ll x ≈ y ∧ emp | x → (z, nil), ls(z, y) ls a (x, y) := S ll x ≈ y ∧ emp | ¬(x ≈ y) ∧ x → (z, nil), ls a (z, y) lls(x, v) := S ll x ≈ v ∧ emp | x → (z, u) * w → (v, nil), ls(u, v), lls(z, w) lls a (x, v) := S ll x ≈ v ∧ emp | x → (z, u) * w → (v, nil), ls a (u, v), lls a (z, w)

  ls a (u 00 , v) ls(u 00 , v) lls a (z 0 , w 0 ) lls(u 0 , w 0 )

A

  Changes Based on the First Round of Reviews • Corrected all typos pointed out by the reviewers; • Page 4, Example 1 -Clearer description of the inductive definitions; • Page 4, paragraph before Example 2 -Referenced the Knaster-Tarski theorem;

Figure 3 :

 3 Figure 3: An NFA-ε equivalent to our default proof strategy S

  |= sl S eo ls o , ls + |= sl S eo ls e or ls

	The entailments ls o |= sl S eo ls + tailments such as ls e |= sl S eo ls	, ls + |= sl S eo ls +	, ls + |= sl S eo ls e , ls o and ls + |= sl S eo ls o do not. A branch of the + |= sl S eo ls e , ls o hold, while en-
	proof for ls + (x, y) ls

+

, ls e

Table 1 :

 1 Experimental results

	LHS	RHS	R	Seq	H Seq HLU HSP	T	CVC4	LHS	RHS	R Seq H Seq HLU HSP	T	CVC4
	tree + 1	tree V 34	7	2	1 0.096s	9	tree tree + 1	I	7	4	1	0 0.033s	7
	tree + 2	tree V 21	7	2	1 0.053s	7	tree tree + 2	I	7	4	1	0 0.028s	5
	tree + 2	tree + 1	V 1477 11	3	2 5.515s 37	tree + 1 tree + 2	I 38 8	2	1 0.096s 14
	ls a	ls	V	8	5	1	0 0.014s	2	ls	ls a I 7	4	1	0 0.015s	2
	lls a	lls	V	21	9	2	1 0.048s	4	lls	lls a I 20 8	2	1 0.043s	4
	ls o	ls +	V	10	6	1	0 0.032s	5	ls e	ls +	I	7	4	1	0 0.024s	4
	ls +	ls +	V	16	8	2	0 0.049s	9	ls e	ls o I 7	4	1	0 0.030s	5
	ls + ls e , ls o V	8	5	1	0 0.020s	4	ls +	ls e	I 13 6	2	0 0.075s	8
	ls +	ls e , ls o V	9	5	1	0 0.028s	8	ls	+	ls o I 20 9	3	0 0.143s 12

/

VolumeXXX (2018)

/ 21 Volume XXX(2018)

AVoCS 2018

/ 21 Volume XXX(2018)

/ 21 Volume XXX(2018)

Volume XXX (2018)

ECEASST

a status update for all of its ancestors.

Algorithm 2 sketches our proof search implementation for R sl Ind , which, given an input sequent p(x) q 1 (x), . . . , q n (x) and an NFA S = (Q S , R sl Ind , T S , q 0 , F S ) describing the proof strategy, explores all derivations rooted at the input sequent. The default strategy is (LU [START_REF] Iosif | Complete Cyclic Proof Systems for Inductive Entailments[END_REF]Theorem 7]. We construct a node Root and add it to the work queue. While the work queue is not empty and the status of Root is Unknown, we dequeue an SNode N. We denote by Q IR N the set of states in S towards which we transition from N.states by applying IR, and build a set R N of applicable inference rule schemata that are also accepted by the strategy.

If AX or ID are in R N and, moreover, their application leads S to transition to some final states, then this branch of the derivation has been successful. We add a leaf, which is marked as Closed. Otherwise, for each IR ∈ R N we consider each instance ir of IR with antecedents

If k = 0 and we reach some final state in S by transition with IR, then this branch is successful and we add a leaf that we mark as Closed. Otherwise, if k > 1, we create an RNode R for ir and an SNode N i for each of its antecedents. If ∆ i = / 0 for some i ∈ [k], then N i is marked as Failed. If this is not the case for any i ∈ [k], then we add N 1 , . . . , N k to the work queue and continue.

When the status of Root changes to Closed, then a proof has been obtained. The proof is extracted from the proof search tree and offered as a certificate. Otherwise, if it changes to Failed, then at least one counterexample has been discovered. We extract the counterexamples from the proof search tree and give them as witnesses. If the work queue becomes empty, but the status of Root is still Unknown, then the proof search was inconclusive and our entire proof search tree is returned as justification.

Case Study: Binary Trees

Consider the following ranked definitions for binary trees. The predicate tree accepts any tree model, tree + 1 accepts trees with at least one node, and tree + 2 accepts trees with at least one node in which the children of a node are either both allocated or both nil.

tree(x)

The entailments tree + 1 |= sl S t tree, tree + 2 |= sl S t tree and tree + 2 |= sl S t tree + 1 hold, facts corroborated by Inductor. A branch of the proof for tree + 2 (x) tree + 1 (x) is depicted below. However, the reversed entailments do not hold and the counterexamples provided are:

• x ≈ nil ∧ emp for tree(x) tree + 1 (x) and tree(x) tree + 2 (x); • x → (l 0 , r 0 ) * tree + 1 (l 0 ) * (r 0 ≈ nil ∧ emp) for tree + 1 (x) tree + 2 (x). Note that predicate atoms can occur within counterexamples and indicate that they can be substituted by any model to obtain a more concrete one. In this case, an immediate substitution with the base case of tree + 1 (l 0 ) gives us x → (l 0 , r 0 ) * l 0 → (nil, nil) * (r 0 ≈ nil ∧ emp), which can be further simplified to x → (l 0 , nil) * l 0 → (nil, nil).