CompCert is a C compiler with a machine-checked mathematical proof of soundness. The Kalray K1c is a very large instruction word (VLIW) in-order core. We extend CompCert for the K1c core. For this, we need some optimizations such as instruction scheduling.
KALRAY-CompCert
We extend the CompCert certified compiler with a backend for the K1C core and various optimizations to reach high performance (instruction scheduling...).
