Commit f9e07fd5 authored by ehilin02's avatar ehilin02
Browse files

intro

parent 261d2c0b
......@@ -13,8 +13,7 @@
%% Title
%\title{Deciding Separation Logic with Pointer Arithmetic and Inductive Definitions}
%\title{Decision Procedures for Heap-lists}
\title{Deciding Separation Logic With \\
Pointer Arithmetic and Heap Lists}
\title{Deciding Separation Logic With Heap Lists}
%%
\author{%
Double Blind
......
......@@ -48,7 +48,7 @@ the satisfiability (but not entailment) problem is decidable.
Nevertheless, none of the aforementioned work is capable of reasoning about heap lists, or generally speaking, pointer arithmetic inside inductive definitions, in a \emph{sound and complete} way. The state-of-the-art static analysis and verification tools, e.g. \cite{CalcagnoDOHY06,Chlipala11,MartiAY06}, resort to sound (but incomplete) heuristics or interactive theorem provers, for reasoning about heap lists.
On the other hand, the decision procedures for ASL or its extensions, e.g. \cite{BrotherstonGK17,DBLP:journals/corr/abs-1802-05935,DBLP:conf/vmcai/Le21}, are unable to tackle heap lists.
%\footnote{The fact that heap lists are beyond the two decidable fragments in~\cite{DBLP:conf/vmcai/Le21} was confirmed by a personal communication with the author of \cite{DBLP:conf/vmcai/Le21}.}.
This motivates us to raise the following research question: \emph{Can decision procedures be achieved for separation logic fragments allowing pointer arithmetic inside inductive definitions}?
This motivates us to raise the following research question: \emph{Can decision procedures be achieved for separation logic fragments allowing heap lists}?
......@@ -134,8 +134,8 @@ lemma.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\mypar{Contribution.}
In this work, we propose decision procedures for a fragment of separation logic called {\slah}, which allows pointer arithmetic inside inductive definitions,
so that inductive predicates specifying heap lists can be defined.
In this work, we propose decision procedures for a fragment of separation logic called {\slah}, which allows some form of pointer arithmetic inside inductive definitions,
so that the inductive predicate specifying heap lists can be defined.
We consider both satisfiability and entailment problems and show that they are NP-complete and coNP-complete respectively.
The decision procedure for satisfiability is obtained by computing an equi-satisfiable abstraction in Presburger arithmetic, whose crux is to show that the summaries of the heap list predicates, which are naturally formalized as existentially quantified non-linear arithmetic formulas, can actually be transformed into Presburger arithmetic formulas.
The decision procedure for entailment, on the other hand, reduces the problem to multiple instances of an ordered entailment problem, where all the address terms of spatial atoms are ordered.
......@@ -143,11 +143,11 @@ The ordered entailment problem is then decided by matching each spatial atom in
Splitting a spatial atom into multiple ones in the antecedent is attributed to pointer arithmetic and unnecessary for SH fragments with nominal addresses.
%Moreover, the availability of $\hls{}$ makes the splitting more involved.
We implemented the decision procedures on top of \cspen\footnote{We anonymize the name of the tool to comply with the double blind procedure.} solver~\cite{GuCW16}.
We implemented the decision procedures on top of \cspen\footnote{We anonymize the name of the tool to comply with the double blind procedure.} 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 (in average, less than 1 second for satisfiability and less than 15 seconds for entailment).
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).\zhilin{The anonymization is properly done.}
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.
......
......@@ -87,8 +87,8 @@
%\newcommand{\cspen}{\textsc{CompSPEN}}
%\newcommand{\cspenp}{\textsc{CompSPEN}$^+$}
\newcommand{\cspen}{\textsc{XXX}}
\newcommand{\cspenp}{\textsc{XXX}$^+$}
\newcommand{\cspen}{\textsc{XYZ}}
\newcommand{\cspenp}{\textsc{XYZ}$^+$}
%%%hide
\newcommand{\hide}[1]{ }
......
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