Putting the Squeeze on Array Programs: Loop Verification via Inductive Rank Reduction

TL;DR

This paper introduces inductive rank reduction, a novel verification method for array programs that simplifies the verification process by reducing array lengths iteratively, enabling automatic correctness proofs even for complex loops.

Contribution

It proposes a new verification technique based on inductive rank reduction, which bypasses the need for loop invariants and automates the process using symbolic execution, Z3, and heuristic synthesis.

Findings

Successfully verified array programs including a bidirectional summation with complex invariants.

Demonstrated the technique's ability to handle programs with non-first-order expressible invariants.

Automated the verification process for array programs with input-dependent lengths.

Abstract

Automatic verification of array manipulating programs is a challenging problem because it often amounts to the inference of in ductive quantified loop invariants which, in some cases, may not even be firstorder expressible. In this paper, we suggest a novel verification tech nique that is based on induction on userdefined rank of program states as an alternative to loopinvariants. Our technique, dubbed inductive rank reduction, works in two steps. Firstly, we simplify the verification problem and prove that the program is correct when the input state con tains an input array of length B or less, using the length of the array as the rank of the state. Secondly, we employ a squeezing function g which converts a program state sigma with an array of length > B to a state g(sigma) containing an array of length minus 1 or less. We prove that when g satisfies certain natural conditions then if the program violates its specification on sigma then it does so also on g(sigma). The correctness of the program on inputs with arrays of arbitrary lengths follows by induction. We make our technique automatic for array programs whose length of execution is proportional to the length of the input arrays by (i) perform ing the first step using symbolic execution, (ii) verifying the conditions required of g using Z3, and (iii) providing a heuristic procedure for syn thesizing g. We implemented our technique and applied it successfully to several interesting arraymanipulating programs, including a bidirec tional summation program whose loop invariant cannot be expressed in firstorder logic while its specification is quantifier free.