Commit cfda8adf authored by Mihaela SIGHIREANU's avatar Mihaela SIGHIREANU
Browse files

small fixes and tricks for references on 1 page

parent 2daa0354
......@@ -189,9 +189,9 @@ We build a heap $h$ from $s$ and $\varphi$ as follows:
%
\item For every predicate atom $\hls{}(t_1,t_2; t_3)$ in $\varphi$, we have $s \models \abs(\hls{}(t_1,t_2; t_3))$. Then either $s(t_1) = s(t_2)$ or $s(t_1) < s(t_2)$ and $s \models \abs^+(\hls{}(x, y; z))[t_1/x, t_2/y, t_3/z]$.
\begin{itemize}
\item For the formal case, let $h(s(t_1))$ undefined.
\item For the first case, we let $h(s(t_1))$ undefined.
\item For the latter case, $s \models (2 = t_3 \wedge t_1 < t_2 \wedge t_2 - t_1 \equiv 0 \bmod 2) \vee (2 < t_3 \wedge 2 \le t_2 - t_1)$.
\item For the second case, $s \models (2 = t_3 \wedge t_1 < t_2 \wedge t_2 - t_1 \equiv 0 \bmod 2) \vee (2 < t_3 \wedge 2 \le t_2 - t_1)$.
\begin{itemize}
\item If $s(t_3) = 2$, then let $h(s(t_1) + 2(i-1)) = 2$ and $h(s(t_1) + 2i-1) = 1$ for every $i: 1 \le i \le \frac{s(t_2) - s(t_1)}{2}$.
\item If $s(t_3) > 2$, then from $s(t_2) - s(t_1) \ge 2$, we know that there is a sequence of numbers $n_1, \cdots, n_\ell$ such that $2 \le n_i \le s(t_3)$ for every $i \in [\ell]$ and $s(t_2) = s(t_1) + \sum \limits_{i \in [\ell]} n_i$. We then let $h(s(t_1) + \sum \limits_{j \in [i-1]} n_j) = n_i$ for every $i \in [\ell]$, and let $h(n') = 1$ for all the other addresses $n' \in [s(t_1), s(t_2)-1]$.
......
......@@ -49,7 +49,12 @@ In Section~\ref{ssec:ent-1}, we consider the special case
The general case is dealt with in Section~\ref{ssec:ent-all};
the procedure calls the special case for the first atom of the consequent with
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. The coNP upper bound is explained in the sequel: 1) the original entailment problem is reduced to at most exponentially many ordered entailment problems since there are exponentially total preorders, 2) each ordered entailment problem can be reduced further to exponentially many special ordered entailment problems where there is one spatial atom in the consequent, 3) the original entailment problem is invalid iff there is an invalid special ordered entailment problem instance, 4) the special ordered entailment problem is in coNP.
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.
The coNP upper bound is explained in the sequel:
1) the original entailment problem is reduced to at most exponentially many ordered entailment problems since there are exponentially many total preorders,
2) each ordered entailment problem can be reduced further to exponentially many special ordered entailment problems where there is one spatial atom in the consequent,
3) the original entailment problem is invalid iff there is an invalid special ordered entailment problem instance,
4) the special ordered entailment problem is in coNP.
%At first, it is easy to observe that if $\abs(\varphi)$ is unsatisfiable,
%then the entailment holds. Moreover, if $\abs(\varphi) \not\models \abs(\psi)$,
......
......@@ -139,9 +139,9 @@ $s,h \models \exists\vec{z}\cdot\Pi:\Sigma$ iff $\exists \vec{n}\in\NN^{|\vec{z
\end{definition}
%\vspace{-2mm}
We write $A \models B$ for $A$ and $B$ (sub-)formula in \slah\ to mean
that $A$ entails $B$, i.e., that for any model $(s,h)$ such that $s,h\models A$
then $s,h\models B$.
We write $A \models B$ for $A$ and $B$ (sub-)formula in \slah\ for
$A$ entails $B$, i.e.,
that for any model $(s,h)$ such that $s,h\models A$ then $s,h\models B$.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......
......@@ -27,8 +27,9 @@ we prefer to keep it in the signature of \PbA\ to obtain quantifier free formula
\PbA\ is a useful tool for showing complexity classes because its
satisfiability problem belongs to various complexity classes depending
on the number of quantifier alternations~\cite{Haase2018ASG}.
In this paper, we consider quantifier-free \PbA\ formulas (abbreviated as \qfpa) and the $\mathsf{\Sigma}_1$-fragment of \PbA (abbreviated as \EPbA), which
contains existentially quantified Presburger arithmetic formulas. The satisfiability problem of {\qfpa} and {\EPbA} is NP-complete.
In this paper, we consider quantifier-free \PbA\ formulas (abbreviated as \qfpa) and the $\mathsf{\Sigma}_1$-fragment of \PbA\ (abbreviated as \EPbA), which
contains existentially quantified Presburger arithmetic formulas.
We recall that the satisfiability problem of {\qfpa} and {\EPbA} is NP-complete.
%When the number of existentially quantified variables is fixed,
%the problem is P-complete.
%Moreover, the existential fragment of \PbA\
......@@ -51,7 +52,7 @@ that encodes its satisfiability:
\begin{compactitem}
\item At first, points-to atoms $t_1 \pto t_2$ are transformed into $\blk(t_1, t_1+1)$.
\item Then, the block atoms $\blk(t_1, t_2)$ are encoded by the constraint $t_1 < t_2$.
\item Also, the predicate atoms $\hls{}(t_1, t_2; t_3)$ are encoded by a formula in {\EPbA}, $t_1 = t_2 \vee \abs^+(\hls{}(t_1, t_2; t_3))$.
\item The predicate atoms $\hls{}(t_1, t_2; t_3)$, absent in ASL, are encoded by a formula in {\EPbA}, $t_1 = t_2 \vee \abs^+(\hls{}(t_1, t_2; t_3))$.
\item Lastly, the separating conjunction is encoded by an {\EPbA} formula constraining the address terms of spatial atoms.
\end{compactitem}
The Appendix~\ref{app:sat-hls} provides more details.
......
......@@ -25,7 +25,7 @@
is 2-EXPTIME hard},
booktitle = {{LPAR}},
series = {EPiCSC},
volume = {73},
OPTvolume = {73},
OPTpages = {191--211},
publisher = {EasyChair},
year = {2020},
......@@ -96,7 +96,7 @@
OPTpages = {400--419},
year = {2006},
series = {LNCS},
volume = {4260},
OPTvolume = {4260},
publisher = {Springer},
doi = {10.1007/11901433\_22},
OPTnote = {Reports on the verification with Coq of the memory allocator of Topsy.
......@@ -216,7 +216,7 @@ series = {ISMM 2020}
@inproceedings{DBLP:conf/tacas/SighireanuPRGIR19,
author = {Mihaela Sighireanu and
Juan Antonio Navarro P{\'{e}}rez and
Juan Antonio P{\'{e}}rez and
Andrey Rybalchenko and
Nikos Gorogiannis and
Radu Iosif and
......@@ -255,7 +255,7 @@ series = {ISMM 2020}
}
@inproceedings{PerezR13,
author = {Juan Antonio Navarro P{\'{e}}rez and
author = {Juan Antonio P{\'{e}}rez and
Andrey Rybalchenko},
title = {Separation Logic Modulo Theories},
booktitle = {{APLAS}},
......@@ -402,7 +402,7 @@ series = {ISMM 2020}
@inproceedings{DBLP:conf/csl/BrotherstonFPG14,
author = {James Brotherston and
Carsten Fuhs and
Juan Antonio Navarro P{\'{e}}rez and
Juan Antonio P{\'{e}}rez and
Nikos Gorogiannis},
OPTeditor = {Thomas A. Henzinger and
Dale Miller},
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment