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 rewriting system on proof trees.
Type de document :
Rapport
[Research Report] RR-6806, INRIA. 2009
Liste complète des métadonnées

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

https://hal.inria.fr/inria-00355778
Contributeur : Clément Hurlin <>
Soumis le : samedi 2 mai 2009 - 12:55:27
Dernière modification le : jeudi 11 janvier 2018 - 16:31:01
Document(s) archivé(s) le : samedi 26 novembre 2016 - 08:39:39

Fichier

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

Identifiants

  • HAL Id : inria-00355778, version 3

Collections

Citation

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

Partager

Métriques

Consultations de la notice

77

Téléchargements de fichiers

67