  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.
