Adapting sequential legacy software to parallel environments can not only save time and money, but additionally avoids the loss of valuable domain knowledge hidden in existing code. A common parallelization approach is the use of standardized parallel design patterns, which allow making best use of parallel programming interfaces such as OpenMP. When such patterns cannot be implemented directly, it can be necessary to apply code transformations beforehand to suitably re-shape the input program. In this paper, we describe how we used Abstract Execution, a semi-automatic program proving technique for second-order program properties, to formally prove the conditional correctness of the restructuring techniques CU Repositioning, Loop Splitting and Geometric Decomposition—for all input programs. The latter two techniques require an advanced modeling technique based on families of abstract location sets.