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.
Type de document :
Communication dans un congrès
Palsberg, Jens and Su, Zhendong. Static Analysis Symposium, Aug 2009, Los Angeles, United States. Springer-Verlag, 5673, pp.52-68, 2009, LNCS
Liste complète des métadonnées

Littérature citée [35 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00380528
Contributeur : Clément Hurlin <>
Soumis le : lundi 17 août 2009 - 16:35:11
Dernière modification le : samedi 27 janvier 2018 - 01:30:52
Document(s) archivé(s) le : samedi 26 novembre 2016 - 11:44:00

Fichier

finalversion.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00380528, version 2

Collections

Citation

Clément Hurlin. Automatic Parallelization and Optimization of Programs by Proof Rewriting. Palsberg, Jens and Su, Zhendong. Static Analysis Symposium, Aug 2009, Los Angeles, United States. Springer-Verlag, 5673, pp.52-68, 2009, LNCS. 〈inria-00380528v2〉

Partager

Métriques

Consultations de la notice

73

Téléchargements de fichiers

92