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

noteInternational audienceRésumé : Le travail présenté dans cet exposé est à l'interface entre la recherche opé-rationnelle et les méthodes formelles. Il s'inscrit dans le cadre du projet Compcert ayantpour but le développement et la véri cation formelle, utilisant l'assistant de preuve Coq,d'un compilateur de langage C potentiellement utilisable pour la production de logicielsembarqués critiques. Nous nous intéressons dans cet exposé à la phase de la compilationconsistant à optimiser l'utilisation des registres du processeur. Nous proposons d'abordercette optimisation en résolvant un problème dit de coloration avec préférences qui généralisedeux problèmes classiques d'optimisation combinatoire : la coloration et la multicoupeminimale. L'algorithme proposé est par ailleurs formellement véri é