@@ -59,11 +59,11 @@ We show how to derive the coNP upper bound from the aforementioned decision proc

%\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.

\end{enumerate}

Therefore, to show that $\varphi\models\psi$ is not valid, we

Therefore, to show that $\varphi\models\psi$ is not valid, the procedure

\begin{itemize}

\item first guess a total preorder and obtain an ordered entailment problem (of polynomial size),

\item then guess for the ordered entailment problem one special ordered entailment problem (of polynomial size) where the consequent contains only one spatial atom,

\item finally guess and verify in polynomial time a polynomial-size witness for the invalidity of the special ordered entailment problem.

\item first guesses a total preorder and obtain an ordered entailment problem (of polynomial size),

\item then guesses for the ordered entailment problem one special ordered entailment problem (of polynomial size) where the consequent contains only one spatial atom,

\item finally guesses and verifies in polynomial time a polynomial-size witness for the invalidity of the special ordered entailment problem.

\end{itemize}

The above procedure runs in nondeterministic polynomial time, thus showing the invalidity of the entailment problem is in NP. From this, we deduce that the entailment problem of {\slah} is in coNP.

Separation Logic (SL, \cite{Reynolds:2002,OHearn19}), an extension of Hoare logic, is a well-established formalism for the verification of heap manipulating programs. SL features a \emph{separating conjunction operator} and \emph{inductive predicates}, which allow to express how data structures are laid out in memory in an abstract way. Since its introduction, various verification tools based on separation logic have been developed. A notable one among them is the INFER tool \cite{CD11}, which was acquired by Facebook in 2013 and has been actively used in its development process \cite{CDD+15}.

Separation Logic (SL, \cite{Reynolds:2002,OHearn19}), an extension of Hoare logic, is a well-established formalism for the verification of heap manipulating programs. SL features a \emph{separating conjunction operator} and \emph{inductive predicates}, which allow to express how data structures are laid out in memory in an abstract way. Since its introduction, various verification tools based on separation logic have been developed. A notable one among them is the INFER tool \cite{CD11}, a static analyzer developed at Facebook and actively used in its development process \cite{CDD+15}.

Decision procedures for separation logic formulas are vital for the automation of the verification process.

@@ -69,15 +69,16 @@ In these analyzers, the decidability of verification problem has not been studie

because these tools employ sound heuristics to solve satisfiability or entailment problems.

Deductive verification of memory allocators has been considered in

several works~\cite{Chlipala11,MartiAY06,AppelN20}.

For example, \cite{Chlipala11} presents a Coq library based on SL that

allows to abstract the low level details of the memory organization

in order to obtain an almost-automatic verification

of an malloc implementation using heap and free lists. However, the

abstraction proposed cannot deal with the coalescing of chunks in the heap lists.

Our logic fragment \slah{} is less general, but allows to reason about the coalescing operation.

several works~\cite{MartiAY06,Chlipala11,AppelN20}.

A heap list based memory allocator is specified and verified using Coq in~\cite{MartiAY06}; the separation logic fragment employed is and extension of \slah{} to deal with the free list.

In order to obtain a mostly-automatic verification of an malloc implementation,

\cite{Chlipala11} defines a Coq library based on SL that

allows to abstract the low level details of the memory organization.

However, the abstraction proposed cannot deal with the coalescing of

chunks in the heap lists. Our logic fragment \slah{} is less general,

but allows to reason automatically about the coalescing operation.

Separation logic is also used in~\cite{AppelN20} to verify the functional correctness

of an malloc implementation Verified Software Toolchain within the Coq proof assistant.

of an malloc implementation using Verified Software Toolchain and Coq.

%A special instance of a memory allocator using chunks of the same size

%has been used in the deductive verification of

% an implementation of the array list collection~\cite{CauderlierS18},

@@ -117,32 +117,13 @@ we define $\abs(\varphi) \triangleq \abs(\Pi:\Sigma)$ since $\exists \vec{z}\cdo

%

The crux of this encoding and

its originality with respect to the ones proposed for ASL in~\cite{BrotherstonGK17}

is the computation of $\abs^+(\hls{}(x, y; z))$.

In the sequel, we show how to compute them.

%Moreover, $\abs(\varphi)$ will be used as a basic ingredient of the entailment procedure in Section~\ref{sec:ent}.

%We tackle this challenge by showing that an {\EPbA} formula can be computed for this purpose, although the summary is a non-linear formula at the first sight.

%by that we recall for self-containment here.

% First, the spatial atoms other than block atoms are translated into $\blk{}$ atoms.

% Second, the non-emptiness and the separation of block atoms is translated

% into an {\EPbA} formula over the boundary terms in $\blk{}$ atoms.

%To exploit this idea, we have to encode the inductive predicate $\hls{}$ as

% a block atom and an additional {\EPbA} formulas, which

% poses the following challenge for the encoding:

% How to compute a least-fixed-point summary of the inductive definition of $\hls{}$.

%We tackle this challenge by showing that an {\EPbA} formula can be computed for this purpose, although the summary is a non-linear formula at the first sight.

%The crux of the aforementioned encoding is to compute $\abs^+(\hls{}(t_1, t_2; t_3))$, which are the least-fixed-point summaries of $\hls{}(t_1, t_2; t_3)$.

is the computation of $\abs^+(\hls{}(x, y; z))$, which is presented in the following.

%

%ESOP'21 Reviewer 3: 4.1 could use a little "closing" text to summarise where we are now: I felt as though we had perhaps already seen the key idea behind the submission (of course, there is more to come); maybe you could reflect on the significance of the Lemma and lead into the next part.

%

%\subsection{{\EPbA} summary of $\hls{}$ atoms}

%%\subsection{{\EPbA} summary of $\hls{}$ atoms}

%\label{ssec:sat-hls-abs}

\smallskip

%\smallskip

Intuitively, the abstraction of the predicate atoms $\hls{}(x, y; z)$

shall summarize the relation between $x$, $y$ and $z$

for all $k \ge1$ unfoldings of the predicate atom.