Sciweavers

Share
JAR
2008

Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves

9 years 7 months ago
Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves
This article describes the formal verification of a compilation algorithm that transforms parallel moves (parallel assignments between variables) into a semanticallyequivalent 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. Keywords Parallel move
Laurence Rideau, Bernard P. Serpette, Xavier Leroy
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2008
Where JAR
Authors Laurence Rideau, Bernard P. Serpette, Xavier Leroy
Comments (0)
books