Formal verification of a program obfuscation based on mixed Boolean-arithmetic expressions. - Sandrine Blazy; Rémi Hutin (CPP, 2019)

Formal verification of a constant-time preserving C compiler. - Gilles Barthe; Sandrine Blazy; Benjamin Grégoire; Rémi Hutin; Vincent Laporte; David Pichardie; Alix Trieu (Proc. ACM Program. Lang., 2020)

Secure Compilation of Constant-Resource Programs. - Gilles Barthe; Sandrine Blazy; Rémi Hutin; David Pichardie (CSF, 2021)

Compilation vérifiée et sécurisée contre les canaux cachés temporels. (Verified Secure Compilation against Timing Side-Channels). - Rémi Hutin (2021)