Color image segmentation based on automatic morphological clustering. - Thierry Géraud; Pierre-Yves Strub; Jérôme Darbon (ICIP (3), 2001)

Building Decision Procedures in the Calculus of Inductive Constructions. - Frédéric Blanqui; Jean-Pierre Jouannaud; Pierre-Yves Strub (CSL, 2007)

From Formal Proofs to Mathematical Proofs: A Safe, Incremental Way for Building in First-order Decision Procedures. - Frédéric Blanqui; Jean-Pierre Jouannaud; Pierre-Yves Strub (IFIP TCS, 2008)

Type Theory and Decision Procedures. (Théorie des Types et Procédures de Décision). - Pierre-Yves Strub (2008)

Coq Modulo Theory. - Pierre-Yves Strub (CSL, 2010)

Modular code-based cryptographic verification. - Cédric Fournet; Markulf Kohlweiss; Pierre-Yves Strub (CCS, 2011)

CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory. - Bruno Barras; Jean-Pierre Jouannaud; Pierre-Yves Strub; Qian Wang (LICS, 2011)

Self-certification: bootstrapping certified typecheckers in F* with Coq. - Pierre-Yves Strub; Nikhil Swamy; Cédric Fournet; Juan Chen 002 (POPL, 2012)

EasyCrypt: A Tutorial. - Gilles Barthe; François Dupressoir; Benjamin Grégoire; César Kunz; Benedikt Schmidt; Pierre-Yves Strub (FOSAD, 2013)

Fully abstract compilation to JavaScript. - Cédric Fournet; Nikhil Swamy; Juan Chen 002; Pierre-Évariste Dagand; Pierre-Yves Strub; Benjamin Livshits (POPL, 2013)

Implementing TLS with Verified Cryptographic Security. - Karthikeyan Bhargavan; Cédric Fournet; Markulf Kohlweiss; Alfredo Pironti 001; Pierre-Yves Strub (IEEE Symposium on Security and Privacy, 2013)

Secure distributed programming with value-dependent types. - Nikhil Swamy; Juan Chen 002; Cédric Fournet; Pierre-Yves Strub; Karthikeyan Bhargavan; Jean Yang 001 (J. Funct. Program., 2013)

Certified Synthesis of Efficient Batch Verifiers. - Joseph A. Akinyele; Gilles Barthe; Benjamin Grégoire; Benedikt Schmidt; Pierre-Yves Strub (CSF, 2014)

Proving Differential Privacy in Hoare Logic. - Gilles Barthe; Marco Gaboardi; Emilio Jesús Gallego Arias; Justin Hsu; César Kunz; Pierre-Yves Strub (CSF, 2014)

A Formal Library for Elliptic Curves in the Coq Proof Assistant. - Evmorfia-Iro Bartzia; Pierre-Yves Strub (ITP, 2014)

Probabilistic relational verification for cryptographic implementations. - Gilles Barthe; Cédric Fournet; Benjamin Grégoire; Pierre-Yves Strub; Nikhil Swamy; Santiago Zanella-Béguelin (POPL, 2014)

Gradual typing embedded securely in JavaScript. - Nikhil Swamy; Cédric Fournet; Aseem Rastogi; Karthikeyan Bhargavan; Juan Chen 002; Pierre-Yves Strub; Gavin M. Bierman (POPL, 2014)

Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS. - Karthikeyan Bhargavan; Antoine Delignat-Lavaud; Cédric Fournet; Alfredo Pironti 001; Pierre-Yves Strub (IEEE Symposium on Security and Privacy, 2014)

Verified Implementations for Secure and Verifiable Computation. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Guillaume Davy; François Dupressoir; Benjamin Grégoire; Pierre-Yves Strub (IACR Cryptol. ePrint Arch., 2014)

Proving the TLS Handshake Secure (as it is). - Karthikeyan Bhargavan; Cédric Fournet; Markulf Kohlweiss; Alfredo Pironti 001; Pierre-Yves Strub; Santiago Zanella-Béguelin (IACR Cryptol. ePrint Arch., 2014)

Relational Reasoning via Probabilistic Coupling. - Gilles Barthe; Thomas Espitau; Benjamin Grégoire; Justin Hsu; Léo Stefanesco; Pierre-Yves Strub (LPAR, 2015)

Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy. - Gilles Barthe; Marco Gaboardi; Emilio Jesús Gallego Arias; Justin Hsu; Aaron Roth 001; Pierre-Yves Strub (POPL, 2015)

Formal Proofs of Transcendence for e and $π$ as an Application of Multivariate and Symmetric Polynomials. - Sophie Bernard; Yves Bertot; Laurence Rideau; Pierre-Yves Strub (CoRR, 2015)

Verified Proofs of Higher-Order Masking. - Gilles Barthe; Sonia Belaïd; François Dupressoir; Pierre-Alain Fouque; Benjamin Grégoire; Pierre-Yves Strub (IACR Cryptol. ePrint Arch., 2015)

Strong Non-Interference and Type-Directed Higher-Order Masking. - Gilles Barthe; Sonia Belaïd; François Dupressoir; Pierre-Alain Fouque; Benjamin Grégoire; Pierre-Yves Strub; Rébecca Zucchini (CCS, 2016)

Differentially Private Bayesian Programming. - Gilles Barthe; Gian Pietro Farina; Marco Gaboardi; Emilio Jesús Gallego Arias; Andy Gordon 001; Justin Hsu; Pierre-Yves Strub (CCS, 2016)

Advanced Probabilistic Couplings for Differential Privacy. - Gilles Barthe; Noémie Fong; Marco Gaboardi; Benjamin Grégoire; Justin Hsu; Pierre-Yves Strub (CCS, 2016)

Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials. - Sophie Bernard; Yves Bertot; Laurence Rideau; Pierre-Yves Strub (CPP, 2016)

A Program Logic for Union Bounds. - Gilles Barthe; Marco Gaboardi; Benjamin Grégoire; Justin Hsu; Pierre-Yves Strub (ICALP, 2016)

Proving Differential Privacy via Probabilistic Couplings. - Gilles Barthe; Marco Gaboardi; Benjamin Grégoire; Justin Hsu; Pierre-Yves Strub (LICS, 2016)

Dependent types and multi-monadic effects in F. - Nikhil Swamy; Catalin Hritcu; Chantal Keller; Aseem Rastogi; Antoine Delignat-Lavaud; Simon Forest; Karthikeyan Bhargavan; Cédric Fournet; Pierre-Yves Strub; Markulf Kohlweiss; Jean Karim Zinzindohoue; Santiago Zanella-Béguelin (POPL, 2016)

Computer-Aided Verification for Mechanism Design. - Gilles Barthe; Marco Gaboardi; Emilio Jesús Gallego Arias; Justin Hsu; Aaron Roth 001; Pierre-Yves Strub (WINE, 2016)

Advanced Probabilistic Couplings for Differential Privacy. - Gilles Barthe; Marco Gaboardi; Benjamin Grégoire; Justin Hsu; Pierre-Yves Strub (CoRR, 2016)

Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model. - Gilles Barthe; François Dupressoir; Sebastian Faust; Benjamin Grégoire; François-Xavier Standaert; Pierre-Yves Strub (IACR Cryptol. ePrint Arch., 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)

*-Liftings for Differential Privacy. - Gilles Barthe; Thomas Espitau; Justin Hsu; Tetsuya Sato 001; Pierre-Yves Strub (ICALP, 2017)

Proving uniformity and independence by self-composition and coupling. - Gilles Barthe; Thomas Espitau; Benjamin Grégoire; Justin Hsu; Pierre-Yves Strub (LPAR, 2017)

Coq without Type Casts: A Complete Proof of Coq Modulo Theory. - Jean-Pierre Jouannaud; Pierre-Yves Strub (LPAR, 2017)

Coupling proofs are probabilistic product programs. - Gilles Barthe; Benjamin Grégoire; Justin Hsu; Pierre-Yves Strub (POPL, 2017)

Machine-Checked Proofs of Privacy for Electronic Voting Protocols. - Véronique Cortier; Constantin Catalin Dragan; François Dupressoir; Benedikt Schmidt; Pierre-Yves Strub; Bogdan Warinschi (IEEE Symposium on Security and Privacy, 2017)

A messy state of the union: taming the composite state machines of TLS. - Benjamin Beurdouche; Karthikeyan Bhargavan; Antoine Delignat-Lavaud; Cédric Fournet; Markulf Kohlweiss; Alfredo Pironti 001; Pierre-Yves Strub; Jean Karim Zinzindohoue (Commun. ACM, 2017)

A relational logic for higher-order programs. - Alejandro Aguirre 001; Gilles Barthe; Marco Gaboardi; Deepak Garg 001; Pierre-Yves Strub (Proc. ACM Program. Lang., 2017)

An Assertion-Based Program Logic for Probabilistic Programs. - Gilles Barthe; Thomas Espitau; Marco Gaboardi; Benjamin Grégoire; Justin Hsu; Pierre-Yves Strub (ESOP, 2018)

hacspec: Towards Verifiable Crypto Standards. - Karthikeyan Bhargavan; Franziskus Kiefer; Pierre-Yves Strub (SSR, 2018)

Improved Parallel Mask Refreshing Algorithms: Generic Solutions with Parametrized Non-Interference & Automated Optimizations. - Gilles Barthe; Sonia Belaïd; François Dupressoir; Pierre-Alain Fouque; Benjamin Grégoire; François-Xavier Standaert; Pierre-Yves Strub (IACR Cryptol. ePrint Arch., 2018)

Computer-aided proofs for multiparty computation with active security. - Helene Haagh; Aleksandr Karbyshev; Sabine Oechsner; Bas Spitters; Pierre-Yves Strub (IACR Cryptol. ePrint Arch., 2018)

Proving expected sensitivity of probabilistic programs. - Gilles Barthe; Thomas Espitau; Benjamin Grégoire; Justin Hsu; Pierre-Yves Strub (Proc. ACM Program. Lang., 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)

Symbolic Methods in Computational Cryptography Proofs. - Gilles Barthe; Benjamin Grégoire; Charlie Jacomme; Steve Kremer; Pierre-Yves Strub (CSF, 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)

A Machine-Checked Proof of Security for AWS Key Management Service. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; Matthew Campagna; Ernie Cohen; Benjamin Grégoire; Vitor Pereira 002; Bernardo Portela; Pierre-Yves Strub; Serdar Tasiran (IACR Cryptol. ePrint Arch., 2019)

Relational ⋆⋆ star-Liftings for Differential Privacy. - Gilles Barthe; Thomas Espitau; Justin Hsu; Tetsuya Sato 001; Pierre-Yves Strub (Log. Methods Comput. Sci., 2019)

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)

Improved parallel mask refreshing algorithms: generic solutions with parametrized non-interference and automated optimizations. - Gilles Barthe; Sonia Belaïd; François Dupressoir; Pierre-Alain Fouque; Benjamin Grégoire; François-Xavier Standaert; Pierre-Yves Strub (J. Cryptogr. Eng., 2020)

Unsolvability of the Quintic Formalized in Dependent Type Theory. - Sophie Bernard; Cyril Cohen; Assia Mahboubi; Pierre-Yves Strub (ITP, 2021)

EasyPQC: Verifying Post-Quantum Cryptography. - Manuel Barbosa; Gilles Barthe; Xiong Fan; Benjamin Grégoire; Shih-Han Hung; Jonathan Katz; Pierre-Yves Strub; Xiaodi Wu 001; Li Zhou 013 (IACR Cryptol. ePrint Arch., 2021)

A drag-and-drop proof tactic. - Pablo Donato; Pierre-Yves Strub; Benjamin Werner (CPP, 2022)

Formal Verification of Saber's Public-Key Encryption Scheme in EasyCrypt. - Andreas Hülsing; Matthias Meijers; Pierre-Yves Strub (IACR Cryptol. ePrint Arch., 2022)

Formalizing the Face Lattice of Polyhedra. - Xavier Allamigeon; Ricardo D. Katz; Pierre-Yves Strub (Log. Methods Comput. Sci., 2022)

A Formal Disproof of Hirsch Conjecture. - Xavier Allamigeon; Quentin Canu; Pierre-Yves Strub (CPP, 2023)

Machine-Checked Security for rmXMSS as in RFC 8391 and $ mathrm {SPHINCS^{+}} $. - Manuel Barbosa; François Dupressoir; Benjamin Grégoire; Andreas Hülsing; Matthias Meijers; Pierre-Yves Strub (CRYPTO (5), 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)

Machine-Checked Security for $ mathrm{XMSS}$ as in RFC 8391 and $ mathrm{SPHINCS}^{+}$. - Manuel Barbosa; François Dupressoir; Benjamin Grégoire; Andreas Hülsing; Matthias Meijers; 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)

CoqQ: Foundational Verification of Quantum Programs. - Li Zhou 013; Gilles Barthe; Pierre-Yves Strub; Junyi Liu 002; Mingsheng Ying (Proc. ACM Program. Lang., 2023)

Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. - Manuel Barbosa; Gilles Barthe; Benjamin Grégoire; Adrien Koutsos; Pierre-Yves Strub (ACM Trans. Priv. Secur., 2023)

High-Performance NTT Hardware Accelerator to Support ML-KEM and ML-DSA. - Dur-e-Shahwar Kundi; Jose Maria Bermudo Mera; Pierre-Yves Strub; Michael Hutter (ASHES@CCS, 2024)

A Tight Security Proof for SPHINCS+, Formally Verified. - Manuel Barbosa; François Dupressoir; Andreas Hülsing; Matthias Meijers; Pierre-Yves Strub (ASIACRYPT (4), 2024)

CV2EC: Getting the Best of Both Worlds. - Bruno Blanchet; Pierre Boutry; Christian Doczkal; Benjamin Grégoire; Pierre-Yves Strub (CSF, 2024)

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)

A Tight Security Proof for $ mathrm{SPHINCS^{+}}$, Formally Verified. - Manuel Barbosa; François Dupressoir; Andreas Hülsing; Matthias Meijers; Pierre-Yves Strub (IACR Cryptol. ePrint Arch., 2024)

Faster Verification of Faster Implementations: Combining Deductive and Circuit-Based Reasoning in EasyCrypt. - José Bacelar Almeida; Gustavo Xavier Delerue Marinho Alves; Manuel Barbosa; Gilles Barthe; Luís Esquível; Vincent Hwang; Tiago Oliveira 004; Hugo Pacheco 001; Peter Schwabe; Pierre-Yves Strub (SP, 2025)