Verifying Array Manipulating Programs by Tiling

TL;DR

This paper introduces Tiler, a verification method that infers array access patterns through tiling to efficiently prove properties of array-manipulating loops, outperforming existing tools.

Contribution

The paper presents a novel tiling-based verification approach that simplifies array property proofs by reducing them to inductive checks on loop slices.

Findings

Tiler outperforms state-of-the-art verification tools on benchmark suites.

The method effectively handles sequential and nested loops.

Array access pattern inference improves verification efficiency.

Abstract

Formally verifying properties of programs that manipulate arrays in loops is computationally challenging. In this paper, we focus on a useful class of such programs, and present a novel property-driven verification method that first infers array access patterns in loops using simple heuristics, and then uses this information to compositionally prove universally quantified assertions about arrays. Specifically, we identify tiles of array accesses patterns in a loop, and use the tiling information to reduce the problem of checking a quantified assertion at the end of a loop to an inductive argument that checks only a slice of the assertion for a single iteration of the loop body. We show that this method can be extended to programs with sequentially composed loops and nested loops as well. We have implemented our method in a tool called Tiler. Initial experiments show that Tiler outperforms several state-of-the-art tools on a suite of interesting benchmarks.