Pierre-Yves Strub
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
50
Venues
16
Active years
2001–2026
Best venue rank
A*
Where they publish
Papers
50 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2026 | ITP | Functional Correctness of an Optimized Modular Inversion Algorithm. | Assia Mahboubi, Guillaume Melquiond, Pierre-Yves Strub, Toms Vallejos Parada |
| 2025 | CCS | Jazzline: Composable CryptoLine Functional Correctness Proofs for Jasmin Programs. | Jos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Lionel Blatter, Gustavo Xavier Delerue Marinho Alves, Joo Diogo Duarte, Benjamin Grgoire, Tiago Oliveira, Miguel Quaresma, Pierre-Yves Strub, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang |
| 2025 | CCS | Formally Verified Correctness Bounds for Lattice-Based Cryptography. | Manuel Barbosa, Matthias J. Kannwischer, Thing-Han Lim, Peter Schwabe, Pierre-Yves Strub |
| 2025 | SP | 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, Lus Esquvel, Vincent Hwang, Tiago Oliveira, Hugo Pacheco, Peter Schwabe, Pierre-Yves Strub |
| 2024 | ASIACRYPT | A Tight Security Proof for SPHINCS | Manuel Barbosa, Franois Dupressoir, Andreas Hlsing, Matthias Meijers, Pierre-Yves Strub |
| 2024 | CRYPTO | 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, Franois Dupressoir, Benjamin Grgoire, Vincent Laporte, Jean-Christophe Lchenet, Cameron Low, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub |
| 2023 | CPP | A Formal Disproof of Hirsch Conjecture. | Xavier Allamigeon, Quentin Canu, Pierre-Yves Strub |
| 2023 | CRYPTO | Machine-Checked Security for rmXMSS as in RFC 8391 and $\mathrm {SPHINCS^{+}} $. | Manuel Barbosa, Franois Dupressoir, Benjamin Grgoire, Andreas Hlsing, Matthias Meijers, Pierre-Yves Strub |
| 2022 | CPP | A drag-and-drop proof tactic. | Pablo Donato, Pierre-Yves Strub, Benjamin Werner |
| 2022 | CRYPTO | Formal Verification of Saber's Public-Key Encryption Scheme in EasyCrypt. | Andreas Hlsing, Matthias Meijers, Pierre-Yves Strub |
| 2021 | CCS | EasyPQC: Verifying Post-Quantum Cryptography. | Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grgoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, Li Zhou |
| 2021 | CCS | Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. | Manuel Barbosa, Gilles Barthe, Benjamin Grgoire, Adrien Koutsos, Pierre-Yves Strub |
| 2021 | ITP | Unsolvability of the Quintic Formalized in Dependent Type Theory. | Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub |
| 2020 | CADE | Formalizing the Face Lattice of Polyhedra. | Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub |
| 2020 | SP | The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. | Jos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grgoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub |
| 2019 | CCS | Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. | Jos Bacelar Almeida, Ccile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, Franois Dupressoir, Benjamin Grgoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, Pierre-Yves Strub |
| 2019 | CCS | A Machine-Checked Proof of Security for AWS Key Management Service. | Jos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grgoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran |
| 2018 | ESOP | An Assertion-Based Program Logic for Probabilistic Programs. | Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grgoire, Justin Hsu, Pierre-Yves Strub |
| 2017 | CCS | Jasmin: High-Assurance and High-Speed Cryptography. | Jos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grgoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, Pierre-Yves Strub |
| 2017 | EuroCrypt | Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model. | Gilles Barthe, Franois Dupressoir, Sebastian Faust, Benjamin Grgoire, Franois-Xavier Standaert, Pierre-Yves Strub |
| 2017 | ICALP | *-Liftings for Differential Privacy. | Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub |
| 2017 | LPAR | Proving uniformity and independence by self-composition and coupling. | Gilles Barthe, Thomas Espitau, Benjamin Grgoire, Justin Hsu, Pierre-Yves Strub |
| 2017 | LPAR | Coq without Type Casts: A Complete Proof of Coq Modulo Theory. | Jean-Pierre Jouannaud, Pierre-Yves Strub |
| 2017 | POPL | Coupling proofs are probabilistic product programs. | Gilles Barthe, Benjamin Grgoire, Justin Hsu, Pierre-Yves Strub |
| 2017 | SP | Machine-Checked Proofs of Privacy for Electronic Voting Protocols. | Vronique Cortier, Constantin Catalin Dragan, Franois Dupressoir, Benedikt Schmidt, Pierre-Yves Strub, Bogdan Warinschi |
| 2016 | CCS | Strong Non-Interference and Type-Directed Higher-Order Masking. | Gilles Barthe, Sonia Belad, Franois Dupressoir, Pierre-Alain Fouque, Benjamin Grgoire, Pierre-Yves Strub, Rbecca Zucchini |
| 2016 | CCS | Differentially Private Bayesian Programming. | Gilles Barthe, Gian Pietro Farina, Marco Gaboardi, Emilio Jess Gallego Arias, Andy Gordon, Justin Hsu, Pierre-Yves Strub |
| 2016 | CCS | Advanced Probabilistic Couplings for Differential Privacy. | Gilles Barthe, Nomie Fong, Marco Gaboardi, Benjamin Grgoire, Justin Hsu, Pierre-Yves Strub |
| 2016 | CPP | 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 |
| 2016 | ICALP | A Program Logic for Union Bounds. | Gilles Barthe, Marco Gaboardi, Benjamin Grgoire, Justin Hsu, Pierre-Yves Strub |
| 2016 | LICS | Proving Differential Privacy via Probabilistic Couplings. | Gilles Barthe, Marco Gaboardi, Benjamin Grgoire, Justin Hsu, Pierre-Yves Strub |
| 2016 | POPL | Dependent types and multi-monadic effects in F. | Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cdric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, Santiago Zanella-Bguelin |
| 2015 | EuroCrypt | Verified Proofs of Higher-Order Masking. | Gilles Barthe, Sonia Belad, Franois Dupressoir, Pierre-Alain Fouque, Benjamin Grgoire, Pierre-Yves Strub |
| 2015 | LPAR | Relational Reasoning via Probabilistic Coupling. | Gilles Barthe, Thomas Espitau, Benjamin Grgoire, Justin Hsu, Lo Stefanesco, Pierre-Yves Strub |
| 2015 | POPL | Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy. | Gilles Barthe, Marco Gaboardi, Emilio Jess Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub |
| 2015 | SP | A Messy State of the Union: Taming the Composite State Machines of TLS. | Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cdric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Jean Karim Zinzindohoue |
| 2014 | CRYPTO | Proving the TLS Handshake Secure (As It Is). | Karthikeyan Bhargavan, Cdric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella-Bguelin |
| 2014 | ITP | A Formal Library for Elliptic Curves in the Coq Proof Assistant. | Evmorfia-Iro Bartzia, Pierre-Yves Strub |
| 2014 | POPL | Probabilistic relational verification for cryptographic implementations. | Gilles Barthe, Cdric Fournet, Benjamin Grgoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella-Bguelin |
| 2014 | POPL | Gradual typing embedded securely in JavaScript. | Nikhil Swamy, Cdric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, Gavin M. Bierman |
| 2014 | SP | Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS. | Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cdric Fournet, Alfredo Pironti, Pierre-Yves Strub |
| 2013 | POPL | Fully abstract compilation to JavaScript. | Cdric Fournet, Nikhil Swamy, Juan Chen, Pierre-variste Dagand, Pierre-Yves Strub, Benjamin Livshits |
| 2013 | SP | Implementing TLS with Verified Cryptographic Security. | Karthikeyan Bhargavan, Cdric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub |
| 2012 | POPL | Self-certification: bootstrapping certified typecheckers in F* with Coq. | Pierre-Yves Strub, Nikhil Swamy, Cdric Fournet, Juan Chen |
| 2011 | CCS | Modular code-based cryptographic verification. | Cdric Fournet, Markulf Kohlweiss, Pierre-Yves Strub |
| 2011 | ICFP | Secure distributed programming with value-dependent types. | Nikhil Swamy, Juan Chen, Cdric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang |
| 2011 | LICS | 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 |
| 2010 | CSL | Coq Modulo Theory. | Pierre-Yves Strub |
| 2007 | CSL | Building Decision Procedures in the Calculus of Inductive Constructions. | Frdric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub |
| 2001 | ICIP | Color image segmentation based on automatic morphological clustering. | Thierry Graud, Pierre-Yves Strub, Jrme Darbon |