Coloration avec préférences : complexité, inégalités valides et vérification formelle

Benoît Robillard 1 Sandrine Blazy 1, 2 Eric Soutif 1
1 CEDRIC - Centre d'étude et de recherche en informatique et communications
2 GALLIUM - Programming languages, types, compilation and proofs
Inria Paris-Rocquencourt
Résumé : Nous nous intéressons à un problème de coloration avec préférences minimale CPM dans les graphes triangulés. Cette étude s'inscrit dans le projet CompCert qui a pour objectif la certification, à l'aide de méthodes formelles, d'un compilateur optimisant du langage C. L'une des optimisations du compilateur certifié est l'allocation des registres du processeur. Optimiser cette allocation de registres revient à résoudre le problème CPM auquel nous nous intéressons. Nous montrons un résultat de complexité concernant CPM et proposons l'amélioration d'une méthode de coupes permettant la résolution de ce problème. Ce travail est une jonction entre la recherche opérationnelle et les méthodes formelles, dans la mesure où nous vérifions formellement par ailleurs la résolution du problème en prouvant correct le développement, hormis la recherche effectuée par le solveur dont la vérification consiste à déterminer a posteriori si la solution proposée est bien correcte.
Type de document :
Communication dans un congrès
Presses Universitaires de l'Université Blaise Pascal. ROADEF'08, 9e congrès de la Société Française de Recherche Opérationnelle et d'Aide à la Décision, Feb 2008, Clermont-Ferrand, France. pp.123-138, 2008
Liste complète des métadonnées
https://hal.inria.fr/inria-00260712
Contributeur : Sandrine Blazy <>
Soumis le : mardi 4 mars 2008 - 18:17:01
Dernière modification le : mardi 13 novembre 2018 - 17:10:02
Document(s) archivé(s) le : vendredi 28 septembre 2012 - 10:36:16

Fichier

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

Identifiants

  • HAL Id : inria-00260712, version 1

Collections

INRIA | INRIA-ROCQ

Citation

Benoît Robillard, Sandrine Blazy, Eric Soutif. Coloration avec préférences : complexité, inégalités valides et vérification formelle. Presses Universitaires de l'Université Blaise Pascal. ROADEF'08, 9e congrès de la Société Française de Recherche Opérationnelle et d'Aide à la Décision, Feb 2008, Clermont-Ferrand, France. pp.123-138, 2008. 〈inria-00260712〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

306

Téléchargements de fichiers

116

Contact


archive-ouverte@inria.fr