We introduce a work-in-progress system for verifying and inferring properties of integer arrays in programs expressed using purely functional parallel array combinators, such as map, reduce, scan (prefix sum), and scatter (parallel write), commonly found in functional data-parallel languages like Accelerate, Futhark, and LIFT. Our system is based on index functions—functions from indices to values—which model the programs and are used to generate queries to an algebraic solver in order to prove properties. The construction of index functions is tenable due to the bulk-operation semantics of array combinators and the purity of the target languages.