Commit 261d2c0b authored by ehilin02's avatar ehilin02
Browse files

abstract

parent 288920d7
%!TEX root = aplas2021.tex
\begin{abstract}
%Pointer arithmetic is widely used in low-level programs, e.g. memory allocators.
Heap list is a data structure used in many memory allocators, to describe the physical layout of the memory.
Pointer arithmetic is widely used in memory allocators. Moreover, heap list is a data structure used in many memory allocators, to describe the layout of the physical memory.
%
%The verification of such programs usually requires simultaneous reasoning about pointer arithmetic and unbounded heap regions.
The specification of the programs in memory allocators usually requires using pointer arithmetic inside inductive definitions to define heap lists. % in memory allocators.
%
In this work, we investigate decision problems for SLAH, a separation logic fragment
that allows some form of pointer arithmetic inside inductive definitions,
thus enabling specification of properties for programs manipulating heap lists.
that allows pointer arithmetic and an inductive definition for heap lists,
%some form of pointer arithmetic inside inductive definitions,
thus enabling specification of properties for programs in memory allocators.
%
Pointer arithmetic inside inductive definitions is challenging for automated reasoning.
Pointer arithmetic inside the inductive definition for heap lists is challenging for automated reasoning.
%
We tackle this challenge and achieve decision procedures for both satisfiability and entailment of SLAH formulas.
% specifying heap lists data structures.
%
The crux of our decision procedure for satisfiability is to compute summaries of inductive definitions capturing heap lists. We show that although the summary is naturally expressed as an existentially quantified non-linear arithmetic formula, it can actually be transformed into an equivalent linear arithmetic formula.
The crux of our decision procedure for satisfiability is to compute summaries of the inductive definition for heap lists. We show that although the summary is naturally expressed as an existentially quantified non-linear arithmetic formula, it can actually be transformed into an equivalent linear arithmetic formula.
%
The decision procedure for entailment, on the other hand, has to match and split the spatial atoms according to the arithmetic relation between address variables.
%
......
......@@ -13,7 +13,8 @@
%% Title
%\title{Deciding Separation Logic with Pointer Arithmetic and Inductive Definitions}
%\title{Decision Procedures for Heap-lists}
\title{Deciding Separation Logic With Heap Lists}
\title{Deciding Separation Logic With \\
Pointer Arithmetic and Heap Lists}
%%
\author{%
Double Blind
......
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