Automatic Parallelization and Optimization of Programs by Proof Rewriting

C. Hurlin

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    6 Citations (Scopus)


    We show how, given a program and its separation logic proof, one can parallelize and optimize this program and transform its proof simultaneously to obtain a proven parallelized and optimized program. To achieve this goal, we present new proof rules for generating proof trees and a rewrite system on proof trees.
    Original languageUndefined
    Title of host publicationThe 16th International Static Analysis Symposium
    EditorsJ. Palsberg, Z. Su
    Place of PublicationBerlin
    Number of pages17
    ISBN (Print)978-3-642-03236-3
    Publication statusPublished - 9 Aug 2009

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag


    • EWI-15321
    • Separation Logic
    • IR-67469
    • Proof-Preserving Optimizations
    • METIS-263832
    • Automatic Parallelization

    Cite this