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.
Document type :
Preprints, Working Papers, ...
Liste complète des métadonnées

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/inria-00176007
Contributor : Laurence Rideau <>
Submitted on : Tuesday, October 2, 2007 - 11:15:14 AM
Last modification on : Friday, May 25, 2018 - 12:02:07 PM
Document(s) archivé(s) le : Thursday, September 27, 2012 - 12:27:07 PM

Files

pmov.pdf
Files produced by the author(s)

Identifiers

  • 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⟩

Share

Metrics

Record views

341

Files downloads

187