## Laurence Rideau, Bernard P. Serpette, and Xavier Leroy.
Tilting at windmills with Coq: formal verification of a compilation
algorithm for parallel moves.
*Journal of Automated Reasoning*, 40(4):307-326, 2008.

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.

[ bib |
Local copy |
At publisher's ]
Back

*This file was generated by
bibtex2html 1.97.*