A version of the CompCert certified compiler with instruction scheduling for pipelined processors and in particular for Kalray VLIW core (with explicit instruction parallelism at the assembly level).
See the 5-minutes video by C. Six, presenting our certified efficient instruction scheduling for the KVX backend.
