HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

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, ...
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/inria-00176007
Contributor : Laurence Rideau Connect in order to contact the contributor
Submitted on : Tuesday, October 2, 2007 - 11:15:14 AM
Last modification on : Friday, January 21, 2022 - 3:15:21 AM
Long-term archiving on: : 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

133

Files downloads

123