On the Equality of Probabilistic Terms. - Gilles Barthe; Marion Daubignard; Bruce M. Kapron; Yassine Lakhnech; Vincent Laporte (LPAR (Dakar), 2010)

Plan B: a buffered memory model for Java. - Delphine Demange; Vincent Laporte; Lei Zhao; Suresh Jagannathan; David Pichardie; Jan Vitek (POPL, 2013)

Formal Verification of a C Value Analysis Based on Abstract Interpretation. - Sandrine Blazy; Vincent Laporte; André Maroneze; David Pichardie (SAS, 2013)

Atomicity Refinement for Verified Compilation. - Suresh Jagannathan; Vincent Laporte; Gustavo Petri; David Pichardie; Jan Vitek (ACM Trans. Program. Lang. Syst., 2014)

A Formally-Verified C Static Analyzer. - Jacques-Henri Jourdan; Vincent Laporte; Sandrine Blazy; Xavier Leroy; David Pichardie (POPL, 2015)

Verified static analyzes for low-level languages. (Vérification d'analyses statiques pour langages de bas niveau). - Vincent Laporte (2015)

A Certified Compiler for Verifiable Computing. - Cédric Fournet; Chantal Keller; Vincent Laporte (CSF, 2016)

An abstract memory functor for verified C static analyzers. - Sandrine Blazy; Vincent Laporte; David Pichardie (ICFP, 2016)

Verified Abstract Interpretation Techniques for Disassembling Low-level Self-modifying Code. - Sandrine Blazy; Vincent Laporte; David Pichardie (J. Autom. Reason., 2016)

Jasmin: High-Assurance and High-Speed Cryptography. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Arthur Blot; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira 004; Hugo Pacheco 001; Benedikt Schmidt; Pierre-Yves Strub (CCS, 2017)

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

A Fast and Verified Software Stack for Secure Function Evaluation. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; François Dupressoir; Benjamin Grégoire; Vincent Laporte; Vitor Pereira 002 (IACR Cryptol. ePrint Arch., 2017)

Provably secure compilation of side-channel countermeasures. - Gilles Barthe; Benjamin Grégoire; Vincent Laporte (IACR Cryptol. ePrint Arch., 2017)

Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic "Constant-Time". - Gilles Barthe; Benjamin Grégoire; Vincent Laporte (CSF, 2018)

Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. - José Bacelar Almeida; Cécile Baritel-Ruet; Manuel Barbosa; Gilles Barthe; François Dupressoir; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira 004; Alley Stoughton; Pierre-Yves Strub (CCS, 2019)

Machine-Checked Proofs for Cryptographic Standards. - José Bacelar Almeida; Cécile Baritel-Ruet; Manuel Barbosa; Gilles Barthe; François Dupressoir; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira 004; Alley Stoughton; Pierre-Yves Strub (IACR Cryptol. ePrint Arch., 2019)

Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Vincent Laporte; Tiago Oliveira 004 (INDOCRYPT, 2020)

The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Benjamin Grégoire; Adrien Koutsos; Vincent Laporte; Tiago Oliveira 004; Pierre-Yves Strub (SP, 2020)

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)

Structured Leakage and Applications to Cryptographic Constant-Time and Cost. - Gilles Barthe; Benjamin Grégoire; Vincent Laporte; Swarn Priya (IACR Cryptol. ePrint Arch., 2021)

Typing High-Speed Cryptography against Spectre v1. - Basavesh Ammanaghatta Shivakumar; Gilles Barthe; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira 004; Swarn Priya; Peter Schwabe; Lucas Tabary-Maujean (IACR Cryptol. ePrint Arch., 2022)

Enforcing fine-grained constant-time policies. - Basavesh Ammanaghatta Shivakumar; Gilles Barthe; Benjamin Grégoire; Vincent Laporte; Swarn Priya (IACR Cryptol. ePrint Arch., 2022)

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)

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)

Protecting cryptographic code against Spectre-RSB. - Santiago Arranz-Olmos; Gilles Barthe; Chitchanok Chuengsatiansup; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira 004; Peter Schwabe; Yuval Yarom; Zhiyuan Zhang 005 (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)

Protecting Cryptographic Code Against Spectre-RSB: (and, in Fact, All Known Spectre Variants). - Santiago Arranz-Olmos; Gilles Barthe; Chitchanok Chuengsatiansup; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira 004; Peter Schwabe; Yuval Yarom; Zhiyuan Zhang 005 (ASPLOS (2), 2025)

Preservation of Speculative Constant-Time by Compilation. - Santiago Arranz-Olmos; Gilles Barthe; Lionel Blatter; Benjamin Grégoire; Vincent Laporte (Proc. ACM Program. Lang., 2025)

Let's DOIT: Using Intel's Extended HW/SW Contract for Secure Compilation of Crypto Code. - Santiago Arranz-Olmos; Gilles Barthe; Benjamin Grégoire; Jan Jancar; Vincent Laporte; Tiago Oliveira 004; Peter Schwabe (IACR Trans. Cryptogr. Hardw. Embed. Syst., 2025)

Protecting cryptographic code against Spectre-RSB. - Santiago Arranz-Olmos; Gilles Barthe; Chitchanok Chuengsatiansup; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira 004; Peter Schwabe; Yuval Yarom; Zhiyuan Zhang 005 (Zenodo, 2025)

Protecting cryptographic code against Spectre-RSB. - Santiago Arranz-Olmos; Gilles Barthe; Chitchanok Chuengsatiansup; Benjamin Grégoire; Vincent Laporte; Tiago Oliveira 004; Peter Schwabe; Yuval Yarom; Zhiyuan Zhang 005 (Zenodo, 2025)