Jean-Christophe Léchenet

16 papers B 4Journal 8Unranked 3
YearRankTypeTitle / Venue / Authors
2026 B conf
Mechanized Dominator Tree Certification.
CPP
Jean-Christophe Léchenet
2024 — conf
Formally Verifying Kyber - Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt.
CRYPTO (2)
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, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub
2024 J jnl
Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt.
IACR Cryptol. ePrint Arch.
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, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub
2024 J jnl
High-assurance zeroization.
IACR Trans. Cryptogr. Hardw. Embed. Syst.
Santiago Arranz-Olmos, Gilles Barthe, Ruben Gonzalez, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Peter Schwabe
2023 J jnl
Efficient computation of arbitrary control dependencies.
Theor. Comput. Sci.
Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall
2023 J jnl
Formally verifying Kyber Episode IV: Implementation correctness.
IACR Trans. Cryptogr. Hardw. Embed. Syst.
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré, Pierre-Yves Strub
2023 J jnl
Formally verifying Kyber Part I: Implementation Correctness.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré, Pierre-Yves Strub
2023 J jnl
High-assurance zeroization.
IACR Cryptol. ePrint Arch.
Santiago Arranz-Olmos, Gilles Barthe, Ruben Gonzalez, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Peter Schwabe
2023 B conf
Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi.
CPP
Benjamin Grégoire, Jean-Christophe Léchenet, Enrico Tassi
2021 J jnl
Power Consumption Analysis of Parallel Algorithms on GPUs.
CoRR
Frédéric Magoulès, Abal-Kassim Cheik Ahamed, Alban Desmaison, Jean-Christophe Léchenet, François Mayer, Haifa Ben Salem, Thomas Zhu
2020 — conf
A Fast Verified Liveness Analysis in SSA Form.
IJCAR (2)
Jean-Christophe Léchenet, Sandrine Blazy, David Pichardie
2018 — —
Certified algorithms for program slicing. (Algorithmes certifiés pour la simplification syntaxique de programmes).
Jean-Christophe Léchenet
2018 J jnl
Cut branches before looking for bugs: certifiably sound verification on relaxed slices.
Formal Aspects Comput.
Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall
2018 B conf
Fast Computation of Arbitrary Control Dependencies.
FASE
Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall
2016 B conf
Cut Branches Before Looking for Bugs: Sound Verification on Relaxed Slices.
FASE
Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall
2014 — conf
Power Consumption Analysis of Parallel Algorithms on GPUs.
HPCC/CSS/ICESS
Frédéric Magoulès, Abal-Kassim Cheik Ahamed, Alban Desmaison, Jean-Christophe Léchenet, François Mayer, Haifa Ben Salem, Thomas Zhu