


default search action
Gilles Barthe
Person information
- affiliation: Max Planck Institute for Security and Privacy, Bochum, Germany
- affiliation (2008 - 2018): IMDEA Software Institute, Spain
- affiliation (1999 - 2008): INRIA, Sophia-Antipolis, France
- affiliation (1998 - 1999): University of Minho, Braga, Portugal
- affiliation (1997 - 1998): Chalmers University, Gothenburg, Sweden
- affiliation (1995 - 1997): Centrum Wiskunde & Informatica, Amsterdam, The Netherlands
- affiliation (1993 - 1995): University of Nijmegen, The Netherlands
- affiliation (PhD 1993): University of Manchester, UK
Refine list

refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2025
- [j65]Martin Avanzini, Gilles Barthe, Davide Davoli, Benjamin Grégoire:
A Quantitative Probabilistic Relational Hoare Logic. Proc. ACM Program. Lang. 9(POPL): 1167-1195 (2025) - [j64]Yingte Xu, Gilles Barthe, Li Zhou:
Automating Equational Proofs in Dirac Notation. Proc. ACM Program. Lang. 9(POPL): 1227-1259 (2025) - [j63]Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte:
Preservation of Speculative Constant-Time by Compilation. Proc. ACM Program. Lang. 9(POPL): 1293-1325 (2025) - 2024
- [j62]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): 5 (2024) - [j61]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): 784-809 (2024) - [j60]Vineet Rajani
, Gilles Barthe
, Deepak Garg
:
A Modal Type Theory of Expected Cost in Higher-Order Probabilistic Programs. Proc. ACM Program. Lang. 8(OOPSLA2): 389-414 (2024) - [j59]Itsaka Rakotonirina
, Gilles Barthe
, Clara Schneidewind
:
Decision and Complexity of Dolev-Yao Hyperproperties. Proc. ACM Program. Lang. 8(POPL): 1913-1944 (2024) - [j58]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): 375-397 (2024) - [c195]Elizaveta Vasilenko
, Niki Vazou
, Gilles Barthe
:
OBRA: Oracle-Based, Relational, Algorithmic Type Verification. APLAS 2024: 283-302 - [c194]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. CCS 2024: 1076-1090 - [c193]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: 384-421 - [c192]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: 143-144 - [c191]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 - [i102]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 abs/2402.00641 (2024) - [i101]Martin Avanzini, Gilles Barthe, Davide Davoli, Benjamin Grégoire:
A quantitative probabilistic relational Hoare logic. CoRR abs/2407.17127 (2024) - [i100]Yingte Xu, Gilles Barthe, Li Zhou:
Automating Equational Proofs in Dirac Notation. CoRR abs/2411.11617 (2024) - [i99]Mingsheng Ying, Li Zhou, Gilles Barthe:
Laws of Quantum Programming. CoRR abs/2412.19463 (2024) - [i98]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: 843 (2024) - [i97]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: 1070 (2024) - [i96]Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte:
Preservation of Speculative Constant-time by Compilation. IACR Cryptol. ePrint Arch. 2024: 1203 (2024) - [i95]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. IACR Cryptol. ePrint Arch. 2024: 2060 (2024) - 2023
- [j57]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): 95:1-95:29 (2023) - [j56]Li Zhou
, Gilles Barthe
, Pierre-Yves Strub
, Junyi Liu
, Mingsheng Ying
:
CoqQ: Foundational Verification of Quantum Programs. Proc. ACM Program. Lang. 7(POPL): 833-865 (2023) - [j55]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): 164-193 (2023) - [j54]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): 41:1-41:34 (2023) - [c190]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) 2023: 358-389 - [c189]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: 1094-1111 - [c188]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: 1753-1770 - [c187]Zhiyuan Zhang
, Gilles Barthe, Chitchanok Chuengsatiansup, Peter Schwabe, Yuval Yarom:
Ultimate SLH: Taking Speculative Load Hardening to the Next Level. USENIX Security Symposium 2023: 7125-7142 - [i94]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: 215 (2023) - [i93]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: 246 (2023) - [i92]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: 1713 (2023) - 2022
- [j53]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: 100736 (2022) - [j52]Elizaveta Vasilenko
, Niki Vazou
, Gilles Barthe
:
Safe couplings: coupled refinement types. Proc. ACM Program. Lang. 6(ICFP): 596-624 (2022) - [j51]Gilles Barthe
, Raphaëlle Crubillé
, Ugo Dal Lago
, Francesco Gavazzo
:
On Feller continuity and full abstraction. Proc. ACM Program. Lang. 6(ICFP): 826-854 (2022) - [j50]Gilles Barthe, Charlie Jacomme, Steve Kremer
:
Universal Equivalence and Majority of Probabilistic Programs over Finite Fields. ACM Trans. Comput. Log. 23(1): 5:1-5:42 (2022) - [c186]Itsaka Rakotonirina, Miguel Ambrona
, Alejandro Aguirre
, Gilles Barthe:
Symbolic Synthesis of Indifferentiability Attacks. AsiaCCS 2022: 667-681 - [c185]Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya:
Enforcing Fine-grained Constant-time Policies. CCS 2022: 83-96 - [c184]Gilles Barthe, Ugo Dal Lago, Giulio Malavolta
, Itsaka Rakotonirina:
Tidy: Symbolic Verification of Timed Cryptographic Protocols. CCS 2022: 263-276 - [c183]Junyi Liu, Li Zhou, Gilles Barthe, Mingsheng Ying
:
Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs. LICS 2022: 4:1-4:13 - [c182]Gilles Barthe, Adrien Koutsos, Solène Mirliaz, David Pichardie, Peter Schwabe:
Semantic Foundations for Cost Analysis of Pipeline-Optimized Programs. SAS 2022: 372-396 - [c181]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. SP 2022: 632-649 - [c180]Sunjay Cauligi, Craig Disselkoen, Daniel Moghimi, Gilles Barthe, Deian Stefan:
SoK: Practical Foundations for Software Spectre Defenses. SP 2022: 666-680 - [i91]Nico Lehmann, Adam T. Geller, Gilles Barthe, Niki Vazou, Ranjit Jhala:
Flux: Liquid Types for Rust. CoRR abs/2207.04034 (2022) - [i90]Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo:
On Feller Continuity and Full Abstraction (Long Version). CoRR abs/2207.10590 (2022) - [i89]Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying:
CoqQ: Foundational Verification of Quantum Programs. CoRR abs/2207.11350 (2022) - [i88]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: 426 (2022) - [i87]Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya:
Enforcing fine-grained constant-time policies. IACR Cryptol. ePrint Arch. 2022: 630 (2022) - [i86]Zhiyuan Zhang, Gilles Barthe, Chitchanok Chuengsatiansup, Peter Schwabe, Yuval Yarom:
Breaking and Fixing Speculative Load Hardening. IACR Cryptol. ePrint Arch. 2022: 715 (2022) - [i85]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: 1270 (2022) - 2021
- [j49]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): 1-30 (2021) - [j48]Martin Avanzini, Gilles Barthe
, Ugo Dal Lago
:
On continuation-passing transformations and expected cost analysis. Proc. ACM Program. Lang. 5(ICFP): 1-30 (2021) - [j47]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): 1-28 (2021) - [j46]Gilles Barthe, Rohit Chadha, Paul Krogmeier, A. Prasad Sistla, Mahesh Viswanathan:
Deciding accuracy of differential privacy schemes. Proc. ACM Program. Lang. 5(POPL): 1-30 (2021) - [j45]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): 189-228 (2021) - [c179]Kiarash Mohammadi, Amir-Hossein Karimi, Gilles Barthe, Isabel Valera
:
Scaling Guarantees for Nearest Counterfactual Explanations. AIES 2021: 177-187 - [c178]Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya:
Structured Leakage and Applications to Cryptographic Constant-Time and Cost. CCS 2021: 462-476 - [c177]Manuel Barbosa
, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub:
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. CCS 2021: 2541-2563 - [c176]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: 2564-2586 - [c175]Gilles Barthe, Sandrine Blazy
, Rémi Hutin, David Pichardie:
Secure Compilation of Constant-Resource Programs. CSF 2021: 1-12 - [c174]Li Zhou
, Gilles Barthe, Justin Hsu, Mingsheng Ying
, Nengkun Yu
:
A Quantum Interpretation of Bunched Logic & Quantum Separation Logic. LICS 2021: 1-14 - [c173]Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, Bryan Parno:
SoK: Computer-Aided Cryptography. SP 2021: 777-795 - [c172]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. SP 2021: 1884-1901 - [i84]Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu:
A Quantum Interpretation of Bunched Logic for Quantum Separation Logic. CoRR abs/2102.00329 (2021) - [i83]Sunjay Cauligi, Craig Disselkoen, Daniel Moghimi, Gilles Barthe, Deian Stefan:
SoK: Practical Foundations for Spectre Defenses. CoRR abs/2105.05801 (2021) - [i82]Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Shin-ya Katsumata, Tetsuya Sato:
Higher-order probabilistic adversarial computations: Categorical semantics and program logics. CoRR abs/2107.01155 (2021) - [i81]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: 156 (2021) - [i80]Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya:
Structured Leakage and Applications to Cryptographic Constant-Time and Cost. IACR Cryptol. ePrint Arch. 2021: 650 (2021) - [i79]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: 1253 (2021) - [i78]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: 1650 (2021) - 2020
- [j44]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): 1685-1729 (2020) - [j43]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): 17-26 (2020) - [j42]Borja Balle, Gilles Barthe, Marco Gaboardi
:
Privacy Profiles and Amplification by Subsampling. J. Priv. Confidentiality 10(1) (2020) - [j41]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): 7:1-7:30 (2020) - [j40]Gilles Barthe, Justin Hsu
, Mingsheng Ying
, Nengkun Yu
, Li Zhou
:
Relational proofs for quantum programs. Proc. ACM Program. Lang. 4(POPL): 21:1-21:29 (2020) - [j39]Gilles Barthe, Justin Hsu
, Kevin Liao:
A probabilistic separation logic. Proc. ACM Program. Lang. 4(POPL): 55:1-55:30 (2020) - [c171]Amir-Hossein Karimi, Gilles Barthe, Borja Balle, Isabel Valera
:
Model-Agnostic Counterfactual Explanations for Consequential Decisions. AISTATS 2020: 895-905 - [c170]Borja Balle, Gilles Barthe, Marco Gaboardi
, Justin Hsu, Tetsuya Sato:
Hypothesis Testing Interpretations and Renyi Differential Privacy. AISTATS 2020: 2496-2506 - [c169]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: 56-83 - [c168]José Bacelar Almeida
, Manuel Barbosa
, Gilles Barthe, Vincent Laporte, Tiago Oliveira
:
Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification. INDOCRYPT 2020: 107-127 - [c167]Gilles Barthe, Rohit Chadha, Vishal Jagannath, A. Prasad Sistla, Mahesh Viswanathan:
Deciding Differential Privacy for Programs with Finite Inputs and Outputs. LICS 2020: 141-154 - [c166]Gilles Barthe, Charlie Jacomme, Steve Kremer
:
Universal equivalence and majority of probabilistic programs over finite fields. LICS 2020: 155-166 - [c165]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: 913-926 - [c164]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. SP 2020: 965-982 - [i77]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 abs/2002.08489 (2020) - [i76]Amir-Hossein Karimi, Gilles Barthe, Bernhard Schölkopf, Isabel Valera:
A survey of algorithmic recourse: definitions, formulations, solutions, and prospects. CoRR abs/2010.04050 (2020) - [i75]Kiarash Mohammadi, Amir-Hossein Karimi, Gilles Barthe, Isabel Valera:
Scaling Guarantees for Nearest Counterfactual Explanations. CoRR abs/2010.04965 (2020) - [i74]Gilles Barthe, Rohit Chadha, Paul Krogmeier, A. Prasad Sistla, Mahesh Viswanathan:
Deciding Accuracy of Differential Privacy Schemes. CoRR abs/2011.06404 (2020) - [i73]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 abs/2011.08069 (2020) - [i72]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: 603 (2020) - [i71]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: 1104 (2020)
2010 – 2019
- 2019
- [j38]Gilles Barthe, Gustavo Betarte
, Juan Diego Campo, Carlos Luna:
System-Level Non-interference of Constant-Time Cryptography. Part I: Model. J. Autom. Reason. 63(1): 1-51 (2019) - [j37]Patrick Baillot, Gilles Barthe, Ugo Dal Lago
:
Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs. J. Autom. Reason. 63(4): 813-855 (2019) - [j36]Alejandro Aguirre
, Gilles Barthe, Marco Gaboardi
, Deepak Garg, Pierre-Yves Strub:
A relational logic for higher-order programs. J. Funct. Program. 29: e16 (2019) - [j35]Gilles Barthe, Edvard Fagerholm, Dario Fiore, John C. Mitchell
, Andre Scedrov, Benedikt Schmidt:
Automated Analysis of Cryptographic Assumptions in Generic Group Models. J. Cryptol. 32(2): 324-360 (2019) - [j34]Gilles Barthe, Christos Dimitrakakis, Marco Gaboardi
, Andreas Haeberlen, Aaron Roth, Aleksandra B. Slavkovic:
Program for TPDP 2016. J. Priv. Confidentiality 9(1) (2019) - [j33]Gilles Barthe, Thomas Espitau, Justin Hsu
, Tetsuya Sato
, Pierre-Yves Strub:
Relational ⋆⋆\star-Liftings for Differential Privacy. Log. Methods Comput. Sci. 15(4) (2019) - [j32]Tetsuya Sato, Alejandro Aguirre
, Gilles Barthe, Marco Gaboardi
, Deepak Garg, Justin Hsu
:
Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization. Proc. ACM Program. Lang. 3(POPL): 38:1-38:30 (2019) - [c163]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: 63-78 - [c162]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: 1607-1622 - [c161]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. CCS 2019: 2147-2164 - [c160]Gilles Barthe, Benjamin Grégoire, Charlie Jacomme, Steve Kremer
, Pierre-Yves Strub:
Symbolic Methods in Computational Cryptography Proofs. CSF 2019: 136-151 - [c159]Gilles Barthe, Sonia Belaïd, Gaëtan Cassiers
, Pierre-Alain Fouque
, Benjamin Grégoire, François-Xavier Standaert
:
maskVerif: Automated Verification of Higher-Order Masking in Presence of Physical Defaults. ESORICS (1) 2019: 300-318 - [c158]Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovács
, Matteo Maffei:
Verifying Relational Properties using Trace Logic. FMCAD 2019: 170-178 - [c157]Tetsuya Sato
, Gilles Barthe, Marco Gaboardi
, Justin Hsu
, Shin-ya Katsumata
:
Approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy. LICS 2019: 1-14 - [c156]Borja Balle, Gilles Barthe, Marco Gaboardi
, Joseph Geumlek:
Privacy Amplification by Mixing and Diffusion Mechanisms. NeurIPS 2019: 13277-13287 - [c155]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: 174-189 - [c154]Ezgi Çiçek, Weihao Qu, Gilles Barthe, Marco Gaboardi
, Deepak Garg:
Bidirectional type checking for relational properties. PLDI 2019: 533-547 - [i70]