CompCert is a C compiler with a machine-checked mathematical proof of soundness. The Kalray KVX core is a very large instruction word (VLIW) in-order core. We extend CompCert for the KVX core. For this, we need some optimizations such as instruction scheduling. See the KVX CompCert Compiler
- PhD Student : Cyril Six
- Supervisors : David Monniaux, Sylvain Boulmé
- Kalray : Benoît Dupont de Dinechin
