| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
Coq à la conquête des moulins
Résumé : Nous presentons la certification formelle en Coq d'un algorithme utilise' dans les compilateurs: l'affectation parallele de registres. Nous proposons deux specifications inductives et une specification fonctionnelle de l'algorithme ainsi que les preuves de correction de ces specifications. Un code fonctionnel ML peut etre extrait de la specification fonctionnelle et integre' au code du compilateur.
https://hal.inria.fr/inria-00001128
Contributor : Laurence Rideau Connect in order to contact the contributor
Submitted on : Tuesday, February 21, 2006 - 4:52:09 PM
Last modification on : Thursday, January 20, 2022 - 5:32:12 PM
Long-term archiving on: : Saturday, April 3, 2010 - 8:08:45 PM
Contributor : Laurence Rideau Connect in order to contact the contributor
Submitted on : Tuesday, February 21, 2006 - 4:52:09 PM
Last modification on : Thursday, January 20, 2022 - 5:32:12 PM
Long-term archiving on: : Saturday, April 3, 2010 - 8:08:45 PM