Tilting at Windmills with Coq: Formal Verification of a Compilation Algorithm for Parallel Moves |
| |
Authors: | Laurence Rideau Bernard Paul Serpette Xavier Leroy |
| |
Affiliation: | (1) INRIA Sophia—Antipolis Méditerranée, B.P. 93, 06902 Sophia-Antipolis, France;(2) INRIA Paris—Rocquencourt, B.P. 105, 78153 Le Chesnay, France |
| |
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. |
| |
Keywords: | Parallel move Parallel assignment Compilation Compiler correctness The Coq proof assistant |
本文献已被 SpringerLink 等数据库收录! |