Automatic Parallelization and Optimization of Programs by Proof Rewriting

Clément Hurlin (1, 2)

1 EVEREST - Environments for Verification and Security of Software
2 FMT group - Formal Methods and Tools

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 rewriting system on proof trees.

Mots clés: Automatic Parallelization; Proof-Preserving Optimizations; Separation Logic

Domaines: Informatique et langage [cs.CL]

Clément Hurlin. Automatic Parallelization and Optimization of Programs by Proof Rewriting. [Research Report] RR-6806, INRIA. 2009. ⟨inria-00355778v3⟩