Parallelizing of software improves its effectiveness and productivity. To guarantee correctness, each new parallel version of the former code must be formally verified to be equivalent to the serial version. We present a novel approach, called GRASSP, that automatically synthesizes parallel versions of software by treating the given serial versions as specifications. GRASSP statically augments an existing serial program with additional functionality to decompose data dependencies in loop iterations, to compute partial results, and to recompose them. In contrast to other parallelizers, GRASSP gradually considers several parallelization scenarios and certifies the results using Horn-based invariant synthesis. For several classes of single-pass array-processing programs, we show that such static parallelization can be performed efficiently. The C++ translations of the GRASSP solutions sped performance by up to 5X relative to serial code on an 8-thread machine and Hadoop translations by up to 10X on a 10-node Amazon EMR cluster.