Gilles Barthe

ORCID

Publication Activity (10 Years)

Years Active: 1995-2024
Publications (10 Years): 183

Top Venues

CoRR

IACR Cryptol. ePrint Arch.

CCS

Proc. ACM Program. Lang.

Publications

Jan Jancar, Marcel Fourné, Daniel De Almeida Braga, Mohamed Sabt, Peter Schwabe, Gilles Barthe, Pierre-Alain Fouque, Yasemin Acar
They're not that hard to mitigate: What Cryptographic Library Developers Think About Timing Attacks. Software Engineering (2024)
Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte
Preservation of Speculative Constant-time by Compilation. IACR Cryptol. ePrint Arch. 2024 (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. IACR Cryptol. ePrint Arch. 2024 (2024)
Martin Avanzini, Gilles Barthe, Davide Davoli, Benjamin Grégoire
A quantitative probabilistic relational Hoare logic. CoRR (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)
Gilles Barthe, Marcel Böhme, Sunjay Cauligi, Chitchanok Chuengsatiansup, Daniel Genkin, Marco Guarnieri, David Mateos Romero, Peter Schwabe, David Wu, Yuval Yarom
Testing side-channel security of cryptographic implementations against future microarchitectures. CoRR (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)
Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque, Benjamin Grégoire, Mélissa Rossi, Mehdi Tibouchi
Masking the GLP Lattice-Based Signature Scheme at Any Order. J. Cryptol. 37 (1) (2024)
Itsaka Rakotonirina, Gilles Barthe, Clara Schneidewind
Decision and Complexity of Dolev-Yao Hyperproperties. Proc. ACM Program. Lang. 8 (POPL) (2024)
Marcel Fourné, Daniel De Almeida Braga, Jan Jancar, Mohamed Sabt, Peter Schwabe, Gilles Barthe, Pierre-Alain Fouque, Yasemin Acar
"These results must be false": A usability evaluation of constant-time analysis tools. USENIX Security Symposium (2024)
Santiago Arranz Olmos, Gilles Barthe, Chitchanok Chuengsatiansup, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Peter Schwabe, Yuval Yarom, Zhiyuan Zhang
Protecting cryptographic code against Spectre-RSB. IACR Cryptol. ePrint Arch. 2024 (2024)
Martin Avanzini, Gilles Barthe, Benjamin Grégoire, Georg Moser, Gabriele Vanoni
Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs. Proc. ACM Program. Lang. 8 (OOPSLA1) (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)
Basavesh Ammanaghatta Shivakumar, Jack Barnes, Gilles Barthe, Sunjay Cauligi, Chitchanok Chuengsatiansup, Daniel Genkin, Sioli O'Connell, Peter Schwabe, Rui Qi Sim, Yuval Yarom
Spectre Declassified: Reading from the Right Place at the Wrong Time. SP (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)
Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. ACM Trans. Priv. Secur. 26 (3) (2023)
Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, Lucas Tabary-Maujean
Typing High-Speed Cryptography against Spectre v1. SP (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)
Amir-Hossein Karimi, Gilles Barthe, Bernhard Schölkopf, Isabel Valera
A Survey of Algorithmic Recourse: Contrastive Explanations and Consequential Recommendations. ACM Comput. Surv. 55 (5) (2023)
Manuel Barbosa, Gilles Barthe, Christian Doczkal, Jelle Don, Serge Fehr, Benjamin Grégoire, Yu-Hsuan Huang, Andreas Hülsing, Yi Lee, Xiaodi Wu
Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium. IACR Cryptol. ePrint Arch. 2023 (2023)
Zhiyuan Zhang, Gilles Barthe, Chitchanok Chuengsatiansup, Peter Schwabe, Yuval Yarom
Ultimate SLH: Taking Speculative Load Hardening to the Next Level. USENIX Security Symposium (2023)
Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying
CoqQ: Foundational Verification of Quantum Programs. Proc. ACM Program. Lang. 7 (POPL) (2023)
Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo
On Feller Continuity and Full Abstraction (Long Version). CoRR (2022)
Manuel Barbosa, Gilles Barthe, Christian Doczkal, Jelle Don, Serge Fehr, Benjamin Grégoire, Yu-Hsuan Huang, Andreas Hülsing, Yi Lee, Xiaodi Wu
Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium. CRYPTO (5) (2022)
Junyi Liu, Li Zhou, Gilles Barthe, Mingsheng Ying
Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs. LICS (2022)
Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo
On Feller continuity and full abstraction. Proc. ACM Program. Lang. 6 (ICFP) (2022)
Gilles Barthe, Adrien Koutsos, Solène Mirliaz, David Pichardie, Peter Schwabe
Semantic Foundations for Cost Analysis of Pipeline-Optimized Programs. SAS (2022)
Jan Jancar, Marcel Fourné, Daniel De Almeida Braga, Mohamed Sabt, Peter Schwabe, Gilles Barthe, Pierre-Alain Fouque, Yasemin Acar
"They're not that hard to mitigate": What Cryptographic Library Developers Think About Timing Attacks. IEEE Symposium on Security and Privacy (2022)
Sunjay Cauligi, Craig Disselkoen, Daniel Moghimi, Gilles Barthe, Deian Stefan
SoK: Practical Foundations for Software Spectre Defenses. IEEE Symposium on Security and Privacy (2022)
Itsaka Rakotonirina, Miguel Ambrona, Alejandro Aguirre, Gilles Barthe
Symbolic Synthesis of Indifferentiability Attacks. AsiaCCS (2022)
Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya
Enforcing fine-grained constant-time policies. IACR Cryptol. ePrint Arch. 2022 (2022)
Zhiyuan Zhang, Gilles Barthe, Chitchanok Chuengsatiansup, Peter Schwabe, Yuval Yarom
Breaking and Fixing Speculative Load Hardening. IACR Cryptol. ePrint Arch. 2022 (2022)
Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying
CoqQ: Foundational Verification of Quantum Programs. CoRR (2022)
Gilles Barthe, Ugo Dal Lago, Giulio Malavolta, Itsaka Rakotonirina
Tidy: Symbolic Verification of Timed Cryptographic Protocols. CCS (2022)
Elizaveta Vasilenko, Niki Vazou, Gilles Barthe
Safe couplings: coupled refinement types. Proc. ACM Program. Lang. 6 (ICFP) (2022)
Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya
Enforcing Fine-grained Constant-time Policies. CCS (2022)
José Carlos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela
A formal treatment of the role of verified compilers in secure computation. J. Log. Algebraic Methods Program. 125 (2022)
Basavesh Ammanaghatta Shivakumar, Jack Barnes, Gilles Barthe, Sunjay Cauligi, Chitchanok Chuengsatiansup, Daniel Genkin, Sioli O'Connell, Peter Schwabe, Rui Qi Sim, Yuval Yarom
Spectre Declassified: Reading from the Right Place at the Wrong Time. IACR Cryptol. ePrint Arch. 2022 (2022)
Gilles Barthe, Charlie Jacomme, Steve Kremer
Universal Equivalence and Majority of Probabilistic Programs over Finite Fields. ACM Trans. Comput. Log. 23 (1) (2022)
Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, Lucas Tabary-Maujean
Typing High-Speed Cryptography against Spectre v1. IACR Cryptol. ePrint Arch. 2022 (2022)
Nico Lehmann, Adam Geller, Gilles Barthe, Niki Vazou, Ranjit Jhala
Flux: Liquid Types for Rust. CoRR (2022)
Gilles Barthe, Sandrine Blazy, Rémi Hutin, David Pichardie
Secure Compilation of Constant-Resource Programs. CSF (2021)
Sunjay Cauligi, Craig Disselkoen, Daniel Moghimi, Gilles Barthe, Deian Stefan
SoK: Practical Foundations for Spectre Defenses. CoRR (2021)
Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu
A Quantum Interpretation of Bunched Logic & Quantum Separation Logic. LICS (2021)
Martin Avanzini, Gilles Barthe, Ugo Dal Lago
On continuation-passing transformations and expected cost analysis. Proc. ACM Program. Lang. 5 (ICFP) (2021)
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Shin-ya Katsumata, Tetsuya Sato
Higher-order probabilistic adversarial computations: Categorical semantics and program logics. CoRR (2021)
Kiarash Mohammadi, Amir-Hossein Karimi, Gilles Barthe, Isabel Valera
Scaling Guarantees for Nearest Counterfactual Explanations. AIES (2021)
Gilles Barthe, Rohit Chadha, Paul Krogmeier, A. Prasad Sistla, Mahesh Viswanathan
Deciding accuracy of differential privacy schemes. Proc. ACM Program. Lang. 5 (POPL) (2021)
Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya
Structured Leakage and Applications to Cryptographic Constant-Time and Cost. IACR Cryptol. ePrint Arch. 2021 (2021)
Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya
Structured Leakage and Applications to Cryptographic Constant-Time and Cost. CCS (2021)
Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, Li Zhou
EasyPQC: Verifying Post-Quantum Cryptography. IACR Cryptol. ePrint Arch. 2021 (2021)
Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu
A Quantum Interpretation of Bunched Logic for Quantum Separation Logic. CoRR (2021)
Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, Tiago Oliveira, Swarn Priya, Tamara Rezk, Peter Schwabe
High-Assurance Cryptography in the Spectre Era. IEEE Symposium on Security and Privacy (2021)
Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
A pre-expectation calculus for probabilistic sensitivity. Proc. ACM Program. Lang. 5 (POPL) (2021)
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Shin-ya Katsumata, Tetsuya Sato
Higher-order probabilistic adversarial computations: categorical semantics and program logics. Proc. ACM Program. Lang. 5 (ICFP) (2021)
Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, Li Zhou
EasyPQC: Verifying Post-Quantum Cryptography. CCS (2021)
Gilles Barthe, Marc Gourjon, Benjamin Grégoire, Maximilian Orlt, Clara Paglialonga, Lars Porth
Masking in Fine-Grained Leakage Models: Construction, Implementation and Verification. IACR Trans. Cryptogr. Hardw. Embed. Syst. 2021 (2) (2021)
Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. CCS (2021)
Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. IACR Cryptol. ePrint Arch. 2021 (2021)
Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, Bryan Parno
SoK: Computer-Aided Cryptography. IEEE Symposium on Security and Privacy (2021)
Jan Jancar, Marcel Fourné, Daniel De Almeida Braga, Mohamed Sabt, Peter Schwabe, Gilles Barthe, Pierre-Alain Fouque, Yasemin Acar
âTheyâre not that hard to mitigateâ: What Cryptographic Library Developers Think About Timing Attacks. IACR Cryptol. ePrint Arch. 2021 (2021)
Gilles Barthe, Justin Hsu, Kevin Liao
A probabilistic separation logic. Proc. ACM Program. Lang. 4 (POPL) (2020)
Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, Tiago Oliveira, Swarn Priya, Tamara Rezk, Peter Schwabe
High-Assurance Cryptography Software in the Spectre Era. IACR Cryptol. ePrint Arch. 2020 (2020)
Amir-Hossein Karimi, Gilles Barthe, Borja Balle, Isabel Valera
Model-Agnostic Counterfactual Explanations for Consequential Decisions. AISTATS (2020)
Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo
On the Versatility of Open Logical Relations - Continuity, Automatic Differentiation, and a Containment Theorem. ESOP (2020)
Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu
Formal verification of a constant-time preserving C compiler. Proc. ACM Program. Lang. 4 (POPL) (2020)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Vincent Laporte, Tiago Oliveira
Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification. INDOCRYPT (2020)
Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, David Pichardie
System-Level Non-interference of Constant-Time Cryptography. Part II: Verified Static Analysis and Stealth Memory. J. Autom. Reason. 64 (8) (2020)
Kiarash Mohammadi, Amir-Hossein Karimi, Gilles Barthe, Isabel Valera
Scaling Guarantees for Nearest Counterfactual Explanations. CoRR (2020)
Borja Balle, Gilles Barthe, Marco Gaboardi, Justin Hsu, Tetsuya Sato
Hypothesis Testing Interpretations and Renyi Differential Privacy. AISTATS (2020)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. IEEE Symposium on Security and Privacy (2020)
Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo
On the Versatility of Open Logical Relations: Continuity, Automatic Differentiation, and a Containment Theorem. CoRR (2020)
Gilles Barthe, Rohit Chadha, Vishal Jagannath, A. Prasad Sistla, Mahesh Viswanathan
Deciding Differential Privacy for Programs with Finite Inputs and Outputs. LICS (2020)
Borja Balle, Gilles Barthe, Marco Gaboardi
Privacy Profiles and Amplification by Subsampling. J. Priv. Confidentiality 10 (1) (2020)
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub
Improved parallel mask refreshing algorithms: generic solutions with parametrized non-interference and automated optimizations. J. Cryptogr. Eng. 10 (1) (2020)
Gilles Barthe, Charlie Jacomme, Steve Kremer
Universal equivalence and majority of probabilistic programs over finite fields. LICS (2020)
Gilles Barthe, Roberta De Viti, Peter Druschel, Deepak Garg, Manuel Gomez-Rodriguez, Pierfrancesco Ingo, Matthew Lentz, Aastha Mehta, Bernhard Schölkopf
PanCast: Listening to Bluetooth Beacons for Epidemic Risk Mitigation. CoRR (2020)
Sunjay Cauligi, Craig Disselkoen, Klaus von Gleissenthall, Dean M. Tullsen, Deian Stefan, Tamara Rezk, Gilles Barthe
Constant-time foundations for the new spectre era. PLDI (2020)
Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, Li Zhou
Relational proofs for quantum programs. Proc. ACM Program. Lang. 4 (POPL) (2020)
Gilles Barthe, Rohit Chadha, Paul Krogmeier, A. Prasad Sistla, Mahesh Viswanathan
Deciding Accuracy of Differential Privacy Schemes. CoRR (2020)
Gilles Barthe, Marc Gourjon, Benjamin Grégoire, Maximilian Orlt, Clara Paglialonga, Lars Porth
Masking in Fine-Grained Leakage Models: Construction, Implementation and Verification. IACR Cryptol. ePrint Arch. 2020 (2020)
Amir-Hossein Karimi, Gilles Barthe, Bernhard Schölkopf, Isabel Valera
A survey of algorithmic recourse: definitions, formulations, solutions, and prospects. CoRR (2020)
Borja Balle, Gilles Barthe, Marco Gaboardi, Joseph Geumlek
Privacy Amplification by Mixing and Diffusion Mechanisms. CoRR (2019)
José Bacelar Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, Pierre-Yves Strub
Machine-Checked Proofs for Cryptographic Standards. IACR Cryptol. ePrint Arch. 2019 (2019)
José Bacelar Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, Pierre-Yves Strub
Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. CCS (2019)
Gilles Barthe, Christos Dimitrakakis, Marco Gaboardi, Andreas Haeberlen, Aaron Roth, Aleksandra B. Slavkovic
Program for TPDP 2016. J. Priv. Confidentiality 9 (1) (2019)
Tetsuya Sato, Gilles Barthe, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata
Approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy. LICS (2019)
Sunjay Cauligi, Gary Soeller, Brian Johannesmeyer, Fraser Brown, Riad S. Wahby, John Renner, Benjamin Grégoire, Gilles Barthe, Ranjit Jhala, Deian Stefan
FaCT: a DSL for timing-sensitive computation. PLDI (2019)
Amir-Hossein Karimi, Gilles Barthe, Borja Balle, Isabel Valera
Model-Agnostic Counterfactual Explanations for Consequential Decisions. CoRR (2019)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran
A Machine-Checked Proof of Security for AWS Key Management Service. IACR Cryptol. ePrint Arch. 2019 (2019)
Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovács, Matteo Maffei
Verifying Relational Properties using Trace Logic. CoRR (2019)
Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub
Relational ⋆⋆\star-Liftings for Differential Privacy. Log. Methods Comput. Sci. 15 (4) (2019)
Borja Balle, Gilles Barthe, Marco Gaboardi, Joseph Geumlek
Privacy Amplification by Mixing and Diffusion Mechanisms. NeurIPS (2019)
Manuel Barbosa, Gilles Barthe, Karthikeyan Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, Bryan Parno
SoK: Computer-Aided Cryptography. IACR Cryptol. ePrint Arch. 2019 (2019)
Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque, Mélissa Rossi, Mehdi Tibouchi
GALACTICS: Gaussian Sampling for Lattice-Based Constant-Time Implementation of Cryptographic Signatures, Revisited. IACR Cryptol. ePrint Arch. 2019 (2019)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran
A Machine-Checked Proof of Security for AWS Key Management Service. CCS (2019)
Gilles Barthe, Rohit Chadha, Vishal Jagannath, A. Prasad Sistla, Mahesh Viswanathan
Automated Methods for Checking Differential Privacy. CoRR (2019)
Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
Kantorovich Continuity of Probabilistic Programs. CoRR (2019)
Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, Li Zhou
Coupling Techniques for Reasoning about Quantum Programs. CoRR (2019)
Gilles Barthe, Benjamin Grégoire, Charlie Jacomme, Steve Kremer, Pierre-Yves Strub
Symbolic Methods in Computational Cryptography Proofs. CSF (2019)

Gilles Barthe.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Gilles Barthe