Program synthesis is the task of automatically constructing a program that implements the given specification. It is intensively studied in this decade, perhaps because of recent progress in constraint solvers and program verifiers. Unfortunately, even state-of-the-art methods tend to fail in generating large programs.

This talk discusses the effectiveness of combining program synthesis with program transformations. One may consider program transformations are merely a subcategory of program synthesis. In reality, they enable us to formally express the outline of the desired program and thereby lead to constructing complicated programs by filling the details by program synthesis. As case studies, we review two methods of automatically parallelizing programs for summarizing values in data structures. One is based on quantifier elimination (Morihata and Matsuzaki, FLOPS 2010 [1]), and the other is a recent proposal based on reverse engineering (Morihata and Sato, PLDI 2021 [2]).