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
