Formal verification of control-flow graph flattening. - Sandrine Blazy; Alix Trieu (CPP, 2016)

Verified Translation Validation of Static Analyses. - Gilles Barthe; Sandrine Blazy; Vincent Laporte; David Pichardie; Alix Trieu (CSF, 2017)

Verifying Constant-Time Implementations in a Verified Compilation Toolchain. (Vérification d'implémentations constant-time dans une chaîne de compilation vérifiée). - Alix Trieu (2018)

Verifying constant-time implementations by abstract interpretation. - Sandrine Blazy; David Pichardie; Alix Trieu (J. Comput. Secur., 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)

Efficient and provable local capability revocation using uninitialized capabilities. - Aïna Linn Georges; Armaël Guéneau; Thomas Van Strydonck; Amin Timany; Alix Trieu; Sander Huyghebaert; Dominique Devriese; Lars Birkedal (Proc. ACM Program. Lang., 2021)

Proving full-system security properties under multiple attacker models on capability machines: Coq mechanization. - Thomas Van Strydonck; Aïna Linn Georges; Armaël Guéneau; Alix Trieu; Amin Timany; Frank Piessens; Lars Birkedal; Dominique Devriese (Zenodo, 2021)

Proving full-system security properties under multiple attacker models on capability machines. - Thomas Van Strydonck; Aïna Linn Georges; Armaël Guéneau; Alix Trieu; Amin Timany; Frank Piessens; Lars Birkedal; Dominique Devriese (CSF, 2022)

Le temps des cerises: efficient temporal stack safety on capability machines using directed capabilities. - Aïna Linn Georges; Alix Trieu; Lars Birkedal (Proc. ACM Program. Lang., 2022)

Le Temps des Cerises: Efficient Temporal Stack Safety on Capability Machines using Directed Capabilities (Artifact). - Aïna Linn Georges; Alix Trieu; Lars Birkedal (Zenodo, 2022)

A Generic Framework to Develop and Verify Security Mechanisms at the Microarchitectural Level: Application to Control-Flow Integrity. - Matthieu Baty; Pierre Wilke; Guillaume Hiet; Arnaud Fontaine; Alix Trieu (CSF, 2023)

Cerise: Program Verification on a Capability Machine in the Presence of Untrusted Code. - Aïna Linn Georges; Armaël Guéneau; Thomas Van Strydonck; Amin Timany; Alix Trieu; Dominique Devriese; Lars Birkedal (J. ACM, 2024)