CompCertSSA
A companion web page

CompCertSSA is built on top of the C CompCert verified compiler, by adding a SSA-based middle-end (conversion to SSA, SSA-based optimizations, destruction of SSA). This web page reports only on the parts of the development specific to this SSA middle-end. The complete development is available below.

Papers

Formalization in Coq