|
 
|
[BRS08a] Vérification formelle d'un algorithme d'allocation de registres par coloration de graphe
Conférence Nationale avec comité de lecture : JFLA'08 Journées Francophones des Langages Applicatifs, January 2008, pp.31-46,
motcle:
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.
Commentaires:
Cette publication a fait l'objet d'une invitation aux 1ères Journées Nationales du GDR GPL,
du 28 au 30 Janvier 2009, à Toulouse (France), où elle a été présentée de nouveau.
BibTeX
| @inproceedings { | |||
| BRS08a, | |||
| title | = | "{Vérification formelle d'un algorithme d'allocation de registres par coloration de graphe}", | |
| author | = | " S. Blazy and B. Robillard and E. Soutil ", | |
| booktitle | = | "{JFLA'08 Journées Francophones des Langages Applicatifs}", | |
| year | = | 2008, | |
| month | = | "January", | |
| pages | = | "31-46", | |
| note | = | "{Cette publication a fait l'objet d'une invitation aux 1ères Journées Nationales du GDR GPL, du 28 au 30 Janvier 2009, à Toulouse (France), où elle a été présentée de nouveau.}", | |
| } | |||
