Coloration avec préférences dans les graphes triangulés ...

Pr´esentation du probl`eme et de son cadre d’´etude
R´esolution du probl`eme
Conclusion et perspectives
Coloration avec pr´ef´erences dans les graphes
triangul´es
V´erification formelle de la r´esolution d’un probl`eme de graphes
´Sandrine Blazy, Benoˆıt Robillard et Eric Soutif
CEDRIC, ´equipes CPR et OC
9 Novembre 2007
´S. Blazy B. Robillard E. Soutif Journ´ees Graphes et Algorithmes 2007Pr´esentation du probl`eme et de son cadre d’´etude
R´esolution du probl`eme
Conclusion et perspectives
Plan
1 Pr´esentation du probl`eme et de son cadre d’´etude
Cadre d’´etude
Allocation de registres
´Etat de l’art
2 R´esolution du probl`eme
D´emarche g´en´erale
Coloration avec pr´ef´erences et multicoupe minimale
´S. Blazy B. Robillard E. Soutif Journ´ees Graphes et Algorithmes 2007Pr´esentation du probl`eme et de son cadre d’´etude Cadre d’´etude
R´esolution du probl`eme Allocation de registres
´Conclusion et perspectives Etat de l’art
Contexte d’´etude
Besoin de logiciels sursˆ (domaines s´ecuritaires)
⇒ D´eveloppement de m´ethodes formelles
Probl`eme La compilation n’est pas sureˆ
⇒ Besoin de compilateurs certifi´es
Besoin de code efficace
⇒ Recours `a la recherche op´erationnelle
´S. Blazy B. Robillard E. Soutif Journ´ees Graphes et Algorithmes 2007Pr´esentation du probl`eme et de son cadre d’´etude Cadre d’´etude
R´esolution du probl`eme Allocation de registres
´Conclusion et perspectives Etat de l’art
Allocation de registres
Ex´ecution de programme
⇒ Acc`es m´emoire par le ...