Automatic Parallelization and Optimization of Programs by Proof Rewriting

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.

• Type: Conference
• Year: 2009
• Where: SAS
• Authors: Clément Hurlin
• Keywords: Formal Methods, Proof Trees, SAS 2009, Separation Logic Proof