Skip to Main content Skip to Navigation
Conference papers

Automatic Parallelization and Optimization of Programs by Proof Rewriting

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [35 references]  Display  Hide  Download

https://hal.inria.fr/inria-00380528
Contributor : Clément Hurlin <>
Submitted on : Monday, August 17, 2009 - 4:35:11 PM
Last modification on : Tuesday, December 8, 2020 - 9:50:00 AM
Long-term archiving on: : Saturday, November 26, 2016 - 11:44:00 AM

File

finalversion.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : inria-00380528, version 2

Collections

Citation

Clément Hurlin. Automatic Parallelization and Optimization of Programs by Proof Rewriting. Static Analysis Symposium, Aug 2009, Los Angeles, United States. pp.52-68. ⟨inria-00380528v2⟩

Share

Metrics

Record views

135

Files downloads

278