Certified and efficient instruction scheduling: application to interlocked VLIW processors. - Cyril Six; Sylvain Boulmé; David Monniaux (Proc. ACM Program. Lang., 2020)

Simple, light, yet formally verified, global common subexpression elimination and loop-invariant code motion. - David Monniaux; Cyril Six (LCTES, 2021)

Compilation optimisante et formellement prouvée pour un processeur VLIW. - Cyril Six (2021)

Formally verified superblock scheduling. - Cyril Six; Léo Gourdin; Sylvain Boulmé; David Monniaux; Justus Fasse; Nicolas Nardino (CPP, 2022)

Formally Verified Loop-Invariant Code Motion and Assorted Optimizations. - David Monniaux; Cyril Six (ACM Trans. Embed. Comput. Syst., 2023)