Jean-Christophe Léchenet

ORCID

Publication Activity (10 Years)

Years Active: 2014-2024
Publications (10 Years): 13

Top Venues

IACR Cryptol. ePrint Arch.

IACR Trans. Cryptogr. Hardw. Embed. Syst.

FASE

CoRR

University of Paris-Saclay, France (PHD)

Education History

University of Paris-Saclay, France

PHD

Publications

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
Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt. IACR Cryptol. ePrint Arch. 2024 (2024)
Santiago Arranz Olmos, Gilles Barthe, Ruben Gonzalez, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Peter Schwabe
High-assurance zeroization. IACR Trans. Cryptogr. Hardw. Embed. Syst. 2024 (1) (2024)
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
Formally Verifying Kyber - Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt. CRYPTO (2) (2024)
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
Formally verifying Kyber Part I: Implementation Correctness. IACR Cryptol. ePrint Arch. 2023 (2023)
Benjamin Grégoire, Jean-Christophe Léchenet, Enrico Tassi
Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi. CPP (2023)
Santiago Arranz Olmos, Gilles Barthe, Ruben Gonzalez, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Peter Schwabe
High-assurance zeroization. IACR Cryptol. ePrint Arch. 2023 (2023)
Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall
Efficient computation of arbitrary control dependencies. Theor. Comput. Sci. 969 (2023)
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
Formally verifying Kyber Episode IV: Implementation correctness. IACR Trans. Cryptogr. Hardw. Embed. Syst. 2023 (3) (2023)
Frédéric Magoulès, Abal-Kassim Cheik Ahamed, Alban Desmaison, Jean-Christophe Léchenet, François Mayer, Haifa Ben Salem, Thomas Zhu
Power Consumption Analysis of Parallel Algorithms on GPUs. CoRR (2021)
Jean-Christophe Léchenet, Sandrine Blazy, David Pichardie
A Fast Verified Liveness Analysis in SSA Form. IJCAR (2) (2020)
Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall
Cut branches before looking for bugs: certifiably sound verification on relaxed slices. Formal Aspects Comput. 30 (1) (2018)
Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall
Fast Computation of Arbitrary Control Dependencies. FASE (2018)
Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall
Cut Branches Before Looking for Bugs: Sound Verification on Relaxed Slices. FASE (2016)
Frédéric Magoulès, Abal-Kassim Cheik Ahamed, Alban Desmaison, Jean-Christophe Léchenet, François Mayer, Haifa Ben Salem, Thomas Zhu
Power Consumption Analysis of Parallel Algorithms on GPUs. HPCC/CSS/ICESS (2014)

Jean-Christophe Léchenet.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Jean-Christophe Léchenet