Pointer arithmetic is widely used in low-level programs, e.g. 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 pointer arithmetic inside inductive definitions, thus enabling specification of properties for programs manipulating heap lists. Pointer arithmetic inside inductive definitions is challenging for automated reasoning. We tackle this challenge and achieve decision procedures for both satisfiability and entailment of SLAH formulas. The crux of our decision procedure for satisfiability is to compute summaries of inductive definitions. 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. 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.

翻译：指针算术在低级程序（如内存分配器）中广泛使用。此类程序的规约通常需要在归纳定义中使用指针算术来定义常见数据结构，例如内存分配器中的堆链表。本文研究SLAH（一种允许在归纳定义中使用指针算术的分离逻辑片段）的判定问题，从而支持对操作堆链表程序的属性进行规约。归纳定义中的指针算术为自动推理带来挑战。我们应对这一挑战，实现了SLAH公式的可满足性与蕴涵判定过程。可满足性判定过程的核心在于计算归纳定义的摘要。我们证明：尽管该摘要自然表述为存在量词化的非线性算术公式，但实际上可转化为等价的线性算术公式。另一方面，蕴涵判定过程需根据地址变量间的算术关系匹配并拆分空间原子。我们报告了这些判定过程的实现，以及它们在解决内存分配器基础构建程序验证问题中的优异表现。