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 , Laboratoire I3S - 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.
Complete list of metadatas

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/inria-00289709
Contributor : Xavier Leroy <>
Submitted on : Monday, June 23, 2008 - 1:45:56 PM
Last modification on : Monday, November 5, 2018 - 3:36:03 PM
Long-term archiving on : Friday, September 28, 2012 - 4:26:33 PM

File

parallel-move.pdf
Files produced by the author(s)

Identifiers

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⟩

Share

Metrics

Record views

433

Files downloads

188