Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves

Laurence Rideau 1 Bernard Serpette 2 Xavier Leroy 3
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
2 OASIS - Active objects, semantics, Internet and security
CRISAM - Inria Sophia Antipolis - Méditerranée , COMRED - COMmunications, Réseaux, systèmes Embarqués et Distribués
Abstract : This article describes the formal verification of a compilation algorithm that transforms parallel moves (parallel assignments between variables) into a semantically-equivalent sequence of elementary moves. Two different specifications of the algorithm are given: an inductive specification and a functional one, each with its correctness proofs. A functional program can then be extracted and integrated in the Compcert verified compiler.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2008, 40 (4), pp.307-326. <10.1007/s10817-007-9096-8>


https://hal.inria.fr/inria-00289709
Contributeur : Xavier Leroy <>
Soumis le : lundi 23 juin 2008 - 13:45:56
Dernière modification le : lundi 5 octobre 2015 - 16:58:53
Document(s) archivé(s) le : vendredi 28 septembre 2012 - 16:26:33

Fichier

parallel-move.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Laurence Rideau, Bernard Serpette, Xavier Leroy. Tilting at windmills with Coq: formal verification of a compilation algorithm for parallel moves. Journal of Automated Reasoning, Springer Verlag, 2008, 40 (4), pp.307-326. <10.1007/s10817-007-9096-8>. <inria-00289709>

Partager

Métriques

Consultations de
la notice

258

Téléchargements du document

88