Automatically Proving Microkernels Free from Privilege Escalation from their Executable. - Olivier Nicole; Matthieu Lemerre; Sébastien Bardin; Xavier Rival (CoRR, 2020)

No Crash, No Exploit: Automated Verification of Embedded Kernels. - Olivier Nicole; Matthieu Lemerre; Sébastien Bardin; Xavier Rival (RTAS, 2021)

Lightweight Shape Analysis Based on Physical Types. - Olivier Nicole; Matthieu Lemerre; Xavier Rival (VMCAI, 2022)

Automated verification of systems code using type-based memory abstractions. (Vérification automatique de code système à l'aide d'abstractions mémoire basées sur le typage). - Olivier Nicole (2022)

MacoCaml: Staging Composable and Compilable Macros. - Ningning Xie; Leo White; Olivier Nicole; Jeremy Yallop (Proc. ACM Program. Lang., 2023)