Automatic Parallelization and Optimization of Programs by Proof Rewriting

C. Hurlin

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

    6 Citations (Scopus)

    Abstract

    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
    PublisherSpringer
    Pages52-68
    Number of pages17
    ISBN (Print)978-3-642-03236-3
    DOIs
    Publication statusPublished - 9 Aug 2009

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Volume5673

    Keywords

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

    Cite this

    Hurlin, C. (2009). Automatic Parallelization and Optimization of Programs by Proof Rewriting. In J. Palsberg, & Z. Su (Eds.), The 16th International Static Analysis Symposium (pp. 52-68). [10.1007/978-3-642-03237-0_6] (Lecture Notes in Computer Science; Vol. 5673). Berlin: Springer. https://doi.org/10.1007/978-3-642-03237-0_6