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

• Type: Journal
• Year: 2008
• Where: JAR
• Authors: Laurence Rideau, Bernard P. Serpette, Xavier Leroy
• Keywords: Compilation Algorithm, Formal Verification, JAR 2008, Parallel Moves