Verification of program parallelization

Saeed Darabi

    Research output: ThesisPhD Thesis - Research UT, graduation UT

    337 Downloads (Pure)


    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.
    Original languageEnglish
    QualificationDoctor of Philosophy
    Awarding Institution
    • University of Twente
    • Huisman, Marieke, Supervisor
    Award date2 Mar 2018
    Place of PublicationEnschede
    Print ISBNs978-90-365-4484-9
    Publication statusPublished - 2 Mar 2018


    Dive into the research topics of 'Verification of program parallelization'. Together they form a unique fingerprint.

    Cite this