Pointer arithmetic is widely used in low-level programs, e.g. memory allocators.

%

%The verification of such programs usually requires simultaneous reasoning about pointer arithmetic and unbounded heap regions.

The specification of such programs usually requires using pointer arithmetic inside inductive definitions to define the common data structures, e.g. heap lists in memory allocators.

The specification of such programs usually requires using pointer arithmetic inside inductive definitions to define the common data structures, e.g. 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,

...

...

@@ -21,7 +21,7 @@ The decision procedure for entailment, on the other hand, has to match and split

%

We report on the implementation of these decision procedures and their

good performance in solving problems issued from the verification of

building block programs used in memory allocators.

building block programs manipulating heap-lists used in memory allocators.

%

\hide{

We study the decidability of the verification problem for