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

Oren Ish Shalom, Shachar Itzhaky, Noam Rinetzky +1

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 cas…