Verification of program parallelization

This thesis presents a set of verification techniques based on permission-based separation logic to reason about the data race freedom and functional correctness of program parallelizations. Our reasoning techniques address different forms of high-level and low-level parallelization. For high-level parallel programs, we first define the Parallel Programming Language (PPL), a simple core language that captures the main features of deterministic parallel programming; then we discuss how PPL programs and consequently, real-world deterministic parallel programs (e.g. OpenMP programs) are verified. For low-level parallel programs, we specifically focus on reasoning about GPGPU kernels. At the end we discuss how the presented verification techniques are chained together to reason about the semantic equivalence of high-level parallel programs where they are automatically transformed to low-level parallel programs by a parallelizing compiler. Thus, effectively enabling a holistic verification solution for such parallelization frameworks.