The goal of unbounded program verification is to discover an inductive invariant that over-approximates all reachable program states and is strong enough to exclude all bad states. Invariant synthesis is often addressed by 1) encoding the program to a system of Constrained Horn clauses (CHC) and 2) employing an SMT-based procedure to check satisfiability of CHCs. However, a solution of such a system is often inexpressible in the constraint language, especially if the program suffers of multiple recursive calls operating on the shared data. This talk presents a technique to synchronize recurrent computations, thus increasing the chances for an invariant to be found.

Our novel notion of the CHC product gives rise to a lightweight iterative algorithm of merging recurrent computations into groups and its applications to automated program synthesis. In particular, we applied the CHC-product transformation to certify solutions delivered by our automatic parallelization tool, called GraSSP. Given an arbitrary segmentation of the input array, GraSSP synthesizes a code to determine a new segmentation of that array which allows computing and merging individual computation results for all segments. The talk focuses on the verification aspect of GraSSP, in which the given serial and synthesized parallel programs are encoded to CHCs, transformed with the CHC-product, and efficiently verified for equivalence using a state-of-the-art CHC solver.