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

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 :
Pré-publication, Document de travail
2007


https://hal.inria.fr/inria-00176007
Contributeur : Laurence Rideau <>
Soumis le : mardi 2 octobre 2007 - 11:15:14
Dernière modification le : mardi 2 octobre 2007 - 14:06:38
Document(s) archivé(s) le : jeudi 27 septembre 2012 - 12:27:07

Fichiers

pmov.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00176007, version 1

Collections

Citation

Laurence Rideau, Bernard Serpette, Xavier Leroy. Battling windmills with Coq: formal verification of a compilation algorithm for parallel moves. 2007. <inria-00176007>

Exporter

Partager

Métriques

Consultations de
la notice

231

Téléchargements du document

115