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.
Contributor : Laurence Rideau <>
Submitted on : Tuesday, October 2, 2007 - 11:15:14 AM
Last modification on : Tuesday, October 2, 2007 - 2:06:38 PM
Document(s) archivé(s) le : Thursday, September 27, 2012 - 12:27:07 PM