Vérification formelle d'un algorithme d'allocation de registres par coloration de graphe

Sandrine Blazy 1 Benoît Robillard 1 Eric Soutif 1
1 CEDRIC - Centre d'étude et de recherche en informatique et communications
Résumé : Le travail présenté dans cet article est à l'interface entre la recherche opérationnelle et les méthodes formelles. Il s'inscrit dans le cadre du projet CompCert ayant pour but le développement et la vérification formelle, utilisant l'assistant de preuve Coq, d'un compilateur du langage C potentiellement utilisable pour la production de logiciels embarqués critiques. Nous nous intéressons dans cet article à l'allocation de registres, qui consiste à optimiser l'utilisation des registres du processeur. Nous proposons d'aborder cette optimisation en la modélisant par un problème dit de coloration avec préférences dont nous vérifions formellement la résolution. Cette vérification prend deux formes : preuve de correction de la spécification Coq pour la première partie de l'algorithme et validation a posteriori pour la seconde.
Type de document :
Communication dans un congrès
JFLA (Journées Francophones des Langages Applicatifs), Jan 2008, Etretat, France. pp.31-46, 2008
Liste complète des métadonnées

Littérature citée [8 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/inria-00202713
Contributeur : Sandrine Blazy <>
Soumis le : lundi 7 janvier 2008 - 22:06:11
Dernière modification le : jeudi 13 septembre 2018 - 15:24:05
Document(s) archivé(s) le : jeudi 27 septembre 2012 - 13:46:54

Fichier

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

Identifiants

  • HAL Id : inria-00202713, version 1

Collections

JFLA08

Citation

Sandrine Blazy, Benoît Robillard, Eric Soutif. Vérification formelle d'un algorithme d'allocation de registres par coloration de graphe. JFLA (Journées Francophones des Langages Applicatifs), Jan 2008, Etretat, France. pp.31-46, 2008. 〈inria-00202713〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

291

Téléchargements de fichiers

82

Contact


archive-ouverte@inria.fr