@@ -37,7 +37,7 @@ The remainder of this section is devoted to the proof of the coNP upper bound.

In a nutshell, we show in Section~\ref{ssec:order}

that the entailment problem $\varphi\models\psi$

can be decomposed into a finite number of ordered entailment problems

can be decomposed into a finite number of \emph{ordered entailment problems}

$\varphi' \models_{\preceq}\psi'$ where

all the terms used as start and end addresses of spatial atoms in $\varphi'$ and $\psi'$

are ordered by a preorder $\preceq$.

...

...

@@ -51,8 +51,9 @@ The general case is dealt with in Section~\ref{ssec:ent-all};

all the compatible prefixes of the antecedent, and

it does a recursive call for the remainders of the consequent and the antecedent. Note that to find all the compatible prefixes of the antecedent, some spatial atoms in the antecedent might be split into several ones. We derive the coNP upper bound from the aforementioned decision procedure as follows:

\begin{enumerate}

\item The original entailment problem is reduced to at most exponentially many ordered entailment problems since there are exponentially many total preorders.

\item Each ordered entailment problem can be reduced further to exponentially many special ordered entailment problems where there is one spatial atom in the consequent.

\item The entailment problem is reduced to at most exponentially many

\emph{ordered entailment problems} since there are exponentially many total preorders.

\item Each ordered entailment problem can be reduced further to exponentially many \emph{special ordered entailment problems} where there is one spatial atom in the consequent.

\item The original entailment problem is invalid iff there is an invalid special ordered entailment problem instance.

\item The special ordered entailment problem is in coNP.

@@ -147,7 +147,7 @@ We implemented the decision procedures on top of \cspen\ solver~\cite{GuCW16}.

We evaluate the performance of the new solver, called {\cspenp}~\cite{CompSpenSite},

on a set of formulas originating from path conditions and verification conditions of programs working on heap lists in memory allocators.

We also randomly generate some formulas, in order to test the scalability of {\cspenp} further.

The experimental results show that {\cspenp} is able to solve the satisfiability and entailment problems for {\slah} efficiently (0.07 seconds for satisfiability and 5.02 seconds for entailment in average).

The experimental results show that {\cspenp} is able to solve the satisfiability and entailment problems for {\slah} efficiently (in average, less than 1 second for satisfiability and less than 15 seconds for entailment).

To the best of our knowledge, this work presents the first decision procedure and automated solver for decision problems in a separation logic fragment allowing both pointer arithmetic and memory blocks inside inductive definitions.

%As mentioned before, the logic ASL was introduced in~\cite{BrotherstonGK17}, but it contains no inductive predicates.