Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

74

SAS
2009
Springer

favoriteEmaildiscussreport

175views Formal Methods» more SAS 2009»

Automatic Parallelization and Optimization of Programs by Proof Rewriting

15 years 10 months ago

Automatic Parallelization and Optimization of Programs by Proof Rewriting

Download www-sop.inria.fr

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.

Clément Hurlin

Real-time Traffic

Formal Methods | Proof Trees | SAS 2009 | Separation Logic Proof |

claim paper

Related Content

» Automatic Parallel Program Generation and Optimization from Data Decompositions

» Formal Sequentialization of Distributed Systems via Program Rewriting

» Automated Termination Proofs for Java Programs with Cyclic Data

» Modular Termination Proofs of Recursive Java Bytecode Programs by Term Rewriting

» Proving SelfStabilization with a Proof Assistant

» Automatically proving the correctness of compiler optimizations

» A Proof of Weak Termination Providing the Right Way to Terminate

» Verification of CRWL Programs with Rewriting Logic

» Graph Rewriting for Hardware Dependent Program Optimizations

Post Info
More Details (n/a)

Added	25 Nov 2009
Updated	25 Nov 2009
Type	Conference
Year	2009
Where	SAS
Authors	Clément Hurlin

Comments (0)