Putting the squeeze on array programs: loop verification via inductive rank reduction
scientific article; zbMATH DE number 7228504