Commit 46ae939e authored by Mihaela SIGHIREANU's avatar Mihaela SIGHIREANU
Browse files

aplas: try to go to 18 pages

parent f11bfafb
%!TEX root = aplas2021.tex
\section{Conclusion}
\section{Related work and conclusion}
\label{sec:conc-hls}
\input{related.tex}
\paragraph{Conclusion.}
\smallskip
\mypar{Conclusion.}
In this work, we investigated \slah, a separation logic fragment that allows pointer arithmetic inside inductive definitions so that the commonly used data structures e.g. heap lists can be defined.
We show that the satisfiability problem of {\slah} is NP-complete and
the entailment problem is coNP-complete.
......
......@@ -123,9 +123,9 @@ classified into four suites, whose sizes are given in Table~\ref{tab-exp}, as fo
%using \textsc{VeriFast} since a lot of lemma has to be proved to be able
%to transform (split, merge) allocated memory blocks in \textsc{VeriFast}.
\smallskip
%\smallskip
\mypar{Experiments.}
We run \cspenp\ over the four benchmark suites, using a Ubuntu-16.04 64-bit lap-top with an Intel Core i5-8250U CPU and 2GB RAM.
We ran \cspenp\ over the four benchmark suites, using a Ubuntu-16.04 64-bit laptop with an Intel Core i5-8250U CPU and 2GB RAM.
The experimental results are summarized in Table~\ref{tab-exp}. We set the timeout to 60 seconds. The statistics of average time and maximum time do not include the time of timeout instances.
To the best of our knowledge, the existing solvers are not able to solve \slah\ formulas that include points-to, block and $\hls{}$ atoms.
The solver SLar~\cite{KimuraT17} was designed to solve entailment problems involving points-to, block, and $\ls{}$ atoms. Nevertheless, we are unable to find a way to access SLar, thus failing to compare with it on ASL formulas.
......
......@@ -118,6 +118,6 @@ Then the decision procedures for the satisfiability and entailment problems are
%
The implementation details and the experimental evaluation
are reported in Section~\ref{sec:exp-hls}.
Section~\ref{sec:conc-hls} provides a summary of related works and concludes.
Section~\ref{sec:conc-hls} provides a summary of related work and concludes.
%by a comparison of our work with existing fragments and its impact on verification of memory allocators.
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