Power Consumption Analysis of Parallel Algorithms on GPUs. - Frédéric Magoulès; Abal-Kassim Cheik Ahamed; Alban Desmaison; Jean-Christophe Léchenet; François Mayer; Haifa Ben Salem; Thomas Zhu (HPCC/CSS/ICESS, 2014)

Cut Branches Before Looking for Bugs: Sound Verification on Relaxed Slices. - Jean-Christophe Léchenet; Nikolai Kosmatov; Pascale Le Gall (FASE, 2016)

Fast Computation of Arbitrary Control Dependencies. - Jean-Christophe Léchenet; Nikolai Kosmatov; Pascale Le Gall (FASE, 2018)

Cut branches before looking for bugs: certifiably sound verification on relaxed slices. - Jean-Christophe Léchenet; Nikolai Kosmatov; Pascale Le Gall (Formal Aspects Comput., 2018)

Certified algorithms for program slicing. (Algorithmes certifiés pour la simplification syntaxique de programmes). - Jean-Christophe Léchenet (2018)

A Fast Verified Liveness Analysis in SSA Form. - Jean-Christophe Léchenet; Sandrine Blazy; David Pichardie (IJCAR (2), 2020)

Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi. - Benjamin Grégoire; Jean-Christophe Léchenet; Enrico Tassi (CPP, 2023)

Formally verifying Kyber Part I: Implementation Correctness. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Benjamin Grégoire; Vincent Laporte; Jean-Christophe Léchenet; Tiago Oliveira 004; Hugo Pacheco 001; Miguel Quaresma; Peter Schwabe; Antoine Séré; Pierre-Yves Strub (IACR Cryptol. ePrint Arch., 2023)

Formally verifying Kyber Episode IV: Implementation correctness. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Benjamin Grégoire; Vincent Laporte; Jean-Christophe Léchenet; Tiago Oliveira 004; Hugo Pacheco 001; Miguel Quaresma; Peter Schwabe; Antoine Séré; Pierre-Yves Strub (IACR Trans. Cryptogr. Hardw. Embed. Syst., 2023)

Efficient computation of arbitrary control dependencies. - Jean-Christophe Léchenet; Nikolai Kosmatov; Pascale Le Gall (Theor. Comput. Sci., 2023)

Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt. - José Bacelar Almeida; Santiago Arranz-Olmos; Manuel Barbosa; Gilles Barthe; François Dupressoir; Benjamin Grégoire; Vincent Laporte; Jean-Christophe Léchenet; Cameron Low; Tiago Oliveira 004; Hugo Pacheco 001; Miguel Quaresma; et al. (IACR Cryptol. ePrint Arch., 2024)

High-assurance zeroization. - Santiago Arranz-Olmos; Gilles Barthe; Ruben Gonzalez; Benjamin Grégoire; Vincent Laporte; Jean-Christophe Léchenet; Tiago Oliveira 004; Peter Schwabe (IACR Trans. Cryptogr. Hardw. Embed. Syst., 2024)