@@ -147,7 +147,7 @@ on a set of formulas originating from path conditions and verification condition

...

@@ -147,7 +147,7 @@ on a set of formulas originating from path conditions and verification condition

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

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.05 seconds for satisfiability and 2.57 seconds for entailment in average).

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

To the best of our knowledge, this work represents the first decision procedures and automated solvers for separation logic fragments allowing pointer arithmetic inside inductive definitions.

To the best of our knowledge, this work presents the first decision procedures and automated solvers for separation logic fragments allowing pointer arithmetic inside inductive definitions.

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

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

%As mentioned before, an extension of ASL with the classic singly linked list $\ls{}$ was considered in~\cite{DBLP:journals/corr/abs-1802-05935}

%As mentioned before, an extension of ASL with the classic singly linked list $\ls{}$ was considered in~\cite{DBLP:journals/corr/abs-1802-05935}

% where the only inductive predicate is the classic singly linked list $\ls{}$.

% where the only inductive predicate is the classic singly linked list $\ls{}$.

Note that $\abs(\varphi)$ can be constructed in polynomial time from $\varphi$.

The formula $\abs(\varphi)$ is constructed in polynomial time from $\varphi$.

Moreover, it is essentially a quantifier-free \PbA\ formula containing modulo constraints $t_1\equiv r \bmod n$; the satisfiability of such formulas is still NP-complete.

%We are using $\abs^+(\hls{}(x, y; z))$ defined above

%We are using $\abs^+(\hls{}(x, y; z))$ defined above

%to obtain in polynomial time an equi-satisfiable \EPbA\ abstraction for a symbolic heap $\varphi$, denoted by $\abs(\varphi)$.

%to obtain in polynomial time an equi-satisfiable \EPbA\ abstraction for a symbolic heap $\varphi$, denoted by $\abs(\varphi)$.

This shows that the satisfiability problem of \slah\ is in NP.

Therefore, the satisfiability problem of \slah\ is in NP.

Moreover, it enables using the off-the-shelf SMT solvers e.g. Z3 to solve the satisfiability problem of \slah\ formulas.

%

%

% ESOP'21, Reviewer 3: At the end of page 10, when discussing the abstraction idea, I wondered to what extent this is related to the decision procedures for ASL itself; is the overall approach new, or is it a similar approach with suitable extensions?

% ESOP'21, Reviewer 3: At the end of page 10, when discussing the abstraction idea, I wondered to what extent this is related to the decision procedures for ASL itself; is the overall approach new, or is it a similar approach with suitable extensions?

%For this reason, we leave

%For this reason, we leave

...

@@ -172,5 +172,7 @@ A \slah\ formula $\varphi$ is satisfiable iff $\abs(\varphi)$ is satisfiable.

...

@@ -172,5 +172,7 @@ A \slah\ formula $\varphi$ is satisfiable iff $\abs(\varphi)$ is satisfiable.

\end{proposition}

\end{proposition}

%\vspace{-2mm}

%\vspace{-2mm}

Notice that $\abs(\varphi)$ is essentially a quantifier-free \PbA\ formula containing modulo constraints $t_1\equiv r \bmod n$. The satisfiability of such formulas is still NP-complete. From now on, we shall assume that {\bf$\abs(\varphi)$ is a quantifier-free \PbA\ formula containing modulo constraints}.

%Notice that $\abs(\varphi)$ is essentially a quantifier-free \PbA\ formula containing modulo constraints $t_1 \equiv r \bmod n$. The satisfiability of such formulas is still NP-complete.

From now on, we shall assume that {\bf$\abs(\varphi)$ is a quantifier-free \PbA\ formula containing modulo constraints}. This enables using the off-the-shelf SMT solvers, e.g. Z3, to solve the satisfiability problem of \slah\ formulas.