When Separation Arithmetic is Enough

doi:10.1007/978-3-032-10794-7_2

When Separation Arithmetic is Enough

2026-01-01

0

PRE

AI

J

Jean-Christophe Filliâtre *

DOI：10.1007/978-3-032-10794-7_2

Original

Original request for help

Save

Abstract

En 中文

In the practice of deductive program verification, it is desirable to make proofs as automated as possible. Today, the best tools for that are SMT solvers, which are able to handle both first-order logic and linear arithmetic. However, SMT solvers are not well suited for inductive reasoning, which is often needed to deal with recursive data structures such as linked lists or trees. In this paper, we propose a technique for specifying and proving imperative programs manipulating pointer-based recursive data structures, which stays within reach of first-order provers. The idea is to map a recursive structure onto a flat integer-indexed sequence, in such a way that separation and frame properties can be expressed using only simple arithmetic relations. We illustrate this approach with two examples: an original variant of list reversal and Morriss algorithm for constant-space traversal of a binary tree.

Keywords:

PROVING POINTER PROGRAMS

When Separation Arithmetic is Enough

Abstract

Journal

Organization