Xavier Leroy - SoftwareThe Compcert verified compiler Web site / Commercial version / Github development Compcert is a moderately optimizing compiler from most of the ISO C 1999 language to PowerPC, ARM and x86 assembly language. It comes accompanied with a Coq proof of semantic preservation, ensuring that the generated assembly code behaves as prescribed by the source code. The whole Compcert development is available u
