When Separation Arithmetic is Enough, or How to Automate the Proof of Programs that Use Pointers

In deductive program verification, the more automated the proofs, the more practical the verification. Today, the best tools for mechanized verification are SMT solvers, due to their combination of first-order logic and linear arithmetic. SMT solvers, however, are not well suited for inductive reasoning, and inductive reasoning is often needed to cater for recursive data structures such as lists or trees. In this article, we show how to specify imperative programs over pointer-based recursive data structures in a way that stays within the reach of first-order provers. The idea is to map a recursive structure onto an 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 various programs over lists, trees, and graphs, ranging from a new in-place list reversal to the Schorr-Waite graph-marking algorithm.