Gilles Barthe

398 papers A* 62A 32B 38C 6Misc 5Journal 177Unranked 63
YearRankTypeTitle / Venue / Authors
2025 J jnl
(Dis)Proving Spectre Security with Speculation-Passing Style.
CoRR
Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Xingyu Xie, Zhiyuan Zhang
2025 J jnl
A Duality Theorem for Classical-Quantum States with Applications to Complete Relational Program Logics.
CoRR
Gilles Barthe, Minbo Gao, Jam Kabeer Ali Khan, Matthijs Muis, Ivan Renison, Keiya Sakabe, Michael Walter, Yingte Xu, Li Zhou
2025 J jnl
A Quantitative Probabilistic Relational Hoare Logic.
Proc. ACM Program. Lang.
Martin Avanzini, Gilles Barthe, Davide Davoli, Benjamin Grégoire
2025 J jnl
Automating Equational Proofs in Dirac Notation.
Proc. ACM Program. Lang.
Yingte Xu, Gilles Barthe, Li Zhou
2025 J jnl
CT-LLVM: Automatic Large-Scale Constant-Time Analysis.
IACR Cryptol. ePrint Arch.
Zhiyuan Zhang, Gilles Barthe
2025 A* conf
Complete Quantum Relational Hoare Logics from Optimal Transport Duality.
LICS
Gilles Barthe, Minbo Gao, Theo Wang, Li Zhou
2025 J jnl
Complete Quantum Relational Hoare Logics from Optimal Transport Duality.
CoRR
Gilles Barthe, Minbo Gao, Theo Wang, Li Zhou
2025 — conf
D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation.
CAV (4)
Yingte Xu, Li Zhou, Gilles Barthe
2025 J jnl
D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation.
CoRR
Yingte Xu, Li Zhou, Gilles Barthe
2025 A* conf
Faster Verification of Faster Implementations: Combining Deductive and Circuit-Based Reasoning in EasyCrypt.
SP
José Bacelar Almeida, Gustavo Xavier Delerue Marinho Alves, Manuel Barbosa, Gilles Barthe, Luís Esquível, Vincent Hwang, Tiago Oliveira, Hugo Pacheco, Peter Schwabe, Pierre-Yves Strub
2025 J jnl
Faster Verification of Faster Implementations: Combining Deductive and Circuit-Based Reasoning in EasyCrypt.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Gustavo Xavier Delerue Marinho Alves, Manuel Barbosa, Gilles Barthe, Luís Esquível, Vincent Hwang, Tiago Oliveira, Hugo Pacheco, Peter Schwabe, Pierre-Yves Strub
2025 A* conf
Jazzline: Composable CryptoLine Functional Correctness Proofs for Jasmin Programs.
CCS
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Lionel Blatter, Gustavo Xavier Delerue Marinho Alves, João Diogo Duarte, Benjamin Grégoire, Tiago Oliveira, Miguel Quaresma, Pierre-Yves Strub, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
2025 J jnl
Let's DOIT: Using Intel's Extended HW/SW Contract for Secure Compilation of Crypto Code.
IACR Cryptol. ePrint Arch.
Santiago Arranz-Olmos, Gilles Barthe, Benjamin Grégoire, Jan Jancar, Vincent Laporte, Tiago Oliveira, Peter Schwabe
2025 J jnl
Let's DOIT: Using Intel's Extended HW/SW Contract for Secure Compilation of Crypto Code.
IACR Trans. Cryptogr. Hardw. Embed. Syst.
Santiago Arranz-Olmos, Gilles Barthe, Benjamin Grégoire, Jan Jancar, Vincent Laporte, Tiago Oliveira, Peter Schwabe
2025 J jnl
Preservation of Speculative Constant-Time by Compilation.
Proc. ACM Program. Lang.
Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte
2025 — conf
Protecting Cryptographic Code Against Spectre-RSB: (and, in Fact, All Known Spectre Variants).
ASPLOS (2)
Santiago Arranz-Olmos, Gilles Barthe, Chitchanok Chuengsatiansup, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Peter Schwabe, Yuval Yarom, Zhiyuan Zhang
2025 J jnl
Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs.
J. ACM
Junyi Liu, Li Zhou, Gilles Barthe, Mingsheng Ying
2025 J jnl
The Jasmin Compiler Preserves Cryptographic Security.
CoRR
Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte, Paolo Torrini
2025 J jnl
Transparent Decompilation for Timing Side-Channel Analyses.
CoRR
Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Sören van der Wall, Zhiyuan Zhang
2025 J jnl
Traq: Estimating the Quantum Cost of Classical Programs.
CoRR
Anurudh Peduri, Gilles Barthe, Michael Walter
2024 A* conf
"These results must be false": A usability evaluation of constant-time analysis tools.
USENIX Security Symposium
Marcel Fourné, Daniel De Almeida Braga, Jan Jancar, Mohamed Sabt, Peter Schwabe, Gilles Barthe, Pierre-Alain Fouque, Yasemin Acar
2024 J jnl
"These results must be false": A usability evaluation of constant-time analysis tools.
IACR Cryptol. ePrint Arch.
Marcel Fourné, Daniel De Almeida Braga, Jan Jancar, Mohamed Sabt, Peter Schwabe, Gilles Barthe, Pierre-Alain Fouque, Yasemin Acar
2024 J jnl
A Modal Type Theory of Expected Cost in Higher-Order Probabilistic Programs.
Proc. ACM Program. Lang.
Vineet Rajani, Gilles Barthe, Deepak Garg
2024 J jnl
A quantitative probabilistic relational Hoare logic.
CoRR
Martin Avanzini, Gilles Barthe, Davide Davoli, Benjamin Grégoire
2024 J jnl
Automating Equational Proofs in Dirac Notation.
CoRR
Yingte Xu, Gilles Barthe, Li Zhou
2024 J jnl
Decision and Complexity of Dolev-Yao Hyperproperties.
Proc. ACM Program. Lang.
Itsaka Rakotonirina, Gilles Barthe, Clara Schneidewind
2024 — conf
Formally Verifying Kyber - Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt.
CRYPTO (2)
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
2024 J jnl
Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt.
IACR Cryptol. ePrint Arch.
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
2024 J jnl
High-assurance zeroization.
IACR Trans. Cryptogr. Hardw. Embed. Syst.
Santiago Arranz-Olmos, Gilles Barthe, Ruben Gonzalez, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Peter Schwabe
2024 J jnl
Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs.
Proc. ACM Program. Lang.
Martin Avanzini, Gilles Barthe, Benjamin Grégoire, Georg Moser, Gabriele Vanoni
2024 J jnl
Laws of Quantum Programming.
CoRR
Mingsheng Ying, Li Zhou, Gilles Barthe
2024 J jnl
Masking the GLP Lattice-Based Signature Scheme at Any Order.
J. Cryptol.
Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque, Benjamin Grégoire, Mélissa Rossi, Mehdi Tibouchi
2024 B conf
OBRA: Oracle-Based, Relational, Algorithmic Type Verification.
APLAS
Elizaveta Vasilenko, Niki Vazou, Gilles Barthe
2024 J jnl
Preservation of Speculative Constant-time by Compilation.
IACR Cryptol. ePrint Arch.
Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte
2024 J jnl
Protecting cryptographic code against Spectre-RSB.
IACR Cryptol. ePrint Arch.
Santiago Arranz-Olmos, Gilles Barthe, Chitchanok Chuengsatiansup, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Peter Schwabe, Yuval Yarom, Zhiyuan Zhang
2024 A* conf
Testing Side-channel Security of Cryptographic Implementations against Future Microarchitectures.
CCS
Gilles Barthe, Marcel Böhme, Sunjay Cauligi, Chitchanok Chuengsatiansup, Daniel Genkin, Marco Guarnieri, David Mateos Romero, Peter Schwabe, David Wu, Yuval Yarom
2024 J jnl
Testing side-channel security of cryptographic implementations against future microarchitectures.
CoRR
Gilles Barthe, Marcel Böhme, Sunjay Cauligi, Chitchanok Chuengsatiansup, Daniel Genkin, Marco Guarnieri, David Mateos Romero, Peter Schwabe, David Wu, Yuval Yarom
2024 C conf
They're not that hard to mitigate: What Cryptographic Library Developers Think About Timing Attacks.
Software Engineering
Jan Jancar, Marcel Fourné, Daniel De Almeida Braga, Mohamed Sabt, Peter Schwabe, Gilles Barthe, Pierre-Alain Fouque, Yasemin Acar
2023 J jnl
A Survey of Algorithmic Recourse: Contrastive Explanations and Consequential Recommendations.
ACM Comput. Surv.
Amir-Hossein Karimi, Gilles Barthe, Bernhard Schölkopf, Isabel Valera
2023 J jnl
CoqQ: Foundational Verification of Quantum Programs.
Proc. ACM Program. Lang.
Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying
2023 — conf
Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium.
CRYPTO (5)
Manuel Barbosa, Gilles Barthe, Christian Doczkal, Jelle Don, Serge Fehr, Benjamin Grégoire, Yu-Hsuan Huang, Andreas Hülsing, Yi Lee, Xiaodi Wu
2023 J jnl
Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium.
IACR Cryptol. ePrint Arch.
Manuel Barbosa, Gilles Barthe, Christian Doczkal, Jelle Don, Serge Fehr, Benjamin Grégoire, Yu-Hsuan Huang, Andreas Hülsing, Yi Lee, Xiaodi Wu
2023 J jnl
Formally verifying Kyber Episode IV: Implementation correctness.
IACR Trans. Cryptogr. Hardw. Embed. Syst.
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
2023 J jnl
Formally verifying Kyber Part I: Implementation Correctness.
IACR Cryptol. ePrint Arch.
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
2023 J jnl
High-assurance zeroization.
IACR Cryptol. ePrint Arch.
Santiago Arranz-Olmos, Gilles Barthe, Ruben Gonzalez, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Peter Schwabe
2023 J jnl
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability.
ACM Trans. Priv. Secur.
Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub
2023 A* conf
Spectre Declassified: Reading from the Right Place at the Wrong Time.
SP
Basavesh Ammanaghatta Shivakumar, Jack Barnes, Gilles Barthe, Sunjay Cauligi, Chitchanok Chuengsatiansup, Daniel Genkin, Sioli O'Connell, Peter Schwabe, Rui Qi Sim, Yuval Yarom
2023 A* conf
Typing High-Speed Cryptography against Spectre v1.
SP
Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, Lucas Tabary-Maujean
2023 A* conf
Ultimate SLH: Taking Speculative Load Hardening to the Next Level.
USENIX Security Symposium
Zhiyuan Zhang, Gilles Barthe, Chitchanok Chuengsatiansup, Peter Schwabe, Yuval Yarom
2022 A* conf
"They're not that hard to mitigate": What Cryptographic Library Developers Think About Timing Attacks.
SP
Jan Jancar, Marcel Fourné, Daniel De Almeida Braga, Mohamed Sabt, Peter Schwabe, Gilles Barthe, Pierre-Alain Fouque, Yasemin Acar
2022 J jnl
A formal treatment of the role of verified compilers in secure computation.
J. Log. Algebraic Methods Program.
José Carlos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela
2022 J jnl
Breaking and Fixing Speculative Load Hardening.
IACR Cryptol. ePrint Arch.
Zhiyuan Zhang, Gilles Barthe, Chitchanok Chuengsatiansup, Peter Schwabe, Yuval Yarom
2022 J jnl
CoqQ: Foundational Verification of Quantum Programs.
CoRR
Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying
2022 A* conf
Enforcing Fine-grained Constant-time Policies.
CCS
Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya
2022 J jnl
Enforcing fine-grained constant-time policies.
IACR Cryptol. ePrint Arch.
Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya
2022 J jnl
Flux: Liquid Types for Rust.
CoRR
Nico Lehmann, Adam T. Geller, Gilles Barthe, Niki Vazou, Ranjit Jhala
2022 J jnl
On Feller Continuity and Full Abstraction (Long Version).
CoRR
Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo
2022 J jnl
On Feller continuity and full abstraction.
Proc. ACM Program. Lang.
Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo
2022 A* conf
Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs.
LICS
Junyi Liu, Li Zhou, Gilles Barthe, Mingsheng Ying
2022 J jnl
Safe couplings: coupled refinement types.
Proc. ACM Program. Lang.
Elizaveta Vasilenko, Niki Vazou, Gilles Barthe
2022 B conf
Semantic Foundations for Cost Analysis of Pipeline-Optimized Programs.
SAS
Gilles Barthe, Adrien Koutsos, Solène Mirliaz, David Pichardie, Peter Schwabe
2022 A* conf
SoK: Practical Foundations for Software Spectre Defenses.
SP
Sunjay Cauligi, Craig Disselkoen, Daniel Moghimi, Gilles Barthe, Deian Stefan
2022 J jnl
Spectre Declassified: Reading from the Right Place at the Wrong Time.
IACR Cryptol. ePrint Arch.
Basavesh Ammanaghatta Shivakumar, Jack Barnes, Gilles Barthe, Sunjay Cauligi, Chitchanok Chuengsatiansup, Daniel Genkin, Sioli O'Connell, Peter Schwabe, Rui Qi Sim, Yuval Yarom
2022 A conf
Symbolic Synthesis of Indifferentiability Attacks.
AsiaCCS
Itsaka Rakotonirina, Miguel Ambrona, Alejandro Aguirre, Gilles Barthe
2022 A* conf
Tidy: Symbolic Verification of Timed Cryptographic Protocols.
CCS
Gilles Barthe, Ugo Dal Lago, Giulio Malavolta, Itsaka Rakotonirina
2022 J jnl
Typing High-Speed Cryptography against Spectre v1.
IACR Cryptol. ePrint Arch.
Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, Lucas Tabary-Maujean
2022 J jnl
Universal Equivalence and Majority of Probabilistic Programs over Finite Fields.
ACM Trans. Comput. Log.
Gilles Barthe, Charlie Jacomme, Steve Kremer
2021 A* conf
A Quantum Interpretation of Bunched Logic & Quantum Separation Logic.
LICS
Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu
2021 J jnl
A Quantum Interpretation of Bunched Logic for Quantum Separation Logic.
CoRR
Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu
2021 J jnl
A pre-expectation calculus for probabilistic sensitivity.
Proc. ACM Program. Lang.
Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2021 J jnl
Deciding accuracy of differential privacy schemes.
Proc. ACM Program. Lang.
Gilles Barthe, Rohit Chadha, Paul Krogmeier, A. Prasad Sistla, Mahesh Viswanathan
2021 A* conf
EasyPQC: Verifying Post-Quantum Cryptography.
CCS
Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, Li Zhou
2021 J jnl
EasyPQC: Verifying Post-Quantum Cryptography.
IACR Cryptol. ePrint Arch.
Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, Li Zhou
2021 A* conf
High-Assurance Cryptography in the Spectre Era.
SP
Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, Tiago Oliveira, Swarn Priya, Tamara Rezk, Peter Schwabe
2021 J jnl
Higher-order probabilistic adversarial computations: Categorical semantics and program logics.
CoRR
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Shin-ya Katsumata, Tetsuya Sato
2021 J jnl
Higher-order probabilistic adversarial computations: categorical semantics and program logics.
Proc. ACM Program. Lang.
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Shin-ya Katsumata, Tetsuya Sato
2021 J jnl
Masking in Fine-Grained Leakage Models: Construction, Implementation and Verification.
IACR Trans. Cryptogr. Hardw. Embed. Syst.
Gilles Barthe, Marc Gourjon, Benjamin Grégoire, Maximilian Orlt, Clara Paglialonga, Lars Porth
2021 A* conf
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability.
CCS
Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub
2021 J jnl
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability.
IACR Cryptol. ePrint Arch.
Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub
2021 J jnl
On continuation-passing transformations and expected cost analysis.
Proc. ACM Program. Lang.
Martin Avanzini, Gilles Barthe, Ugo Dal Lago
2021 C conf
Scaling Guarantees for Nearest Counterfactual Explanations.
AIES
Kiarash Mohammadi, Amir-Hossein Karimi, Gilles Barthe, Isabel Valera
2021 A conf
Secure Compilation of Constant-Resource Programs.
CSF
Gilles Barthe, Sandrine Blazy, Rémi Hutin, David Pichardie
2021 A* conf
SoK: Computer-Aided Cryptography.
SP
Manuel Barbosa, Gilles Barthe, Karthik Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, Bryan Parno
2021 J jnl
SoK: Practical Foundations for Spectre Defenses.
CoRR
Sunjay Cauligi, Craig Disselkoen, Daniel Moghimi, Gilles Barthe, Deian Stefan
2021 A* conf
Structured Leakage and Applications to Cryptographic Constant-Time and Cost.
CCS
Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya
2021 J jnl
Structured Leakage and Applications to Cryptographic Constant-Time and Cost.
IACR Cryptol. ePrint Arch.
Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya
2021 J jnl
“They’re not that hard to mitigate”: What Cryptographic Library Developers Think About Timing Attacks.
IACR Cryptol. ePrint Arch.
Jan Jancar, Marcel Fourné, Daniel De Almeida Braga, Mohamed Sabt, Peter Schwabe, Gilles Barthe, Pierre-Alain Fouque, Yasemin Acar
2020 J jnl
A probabilistic separation logic.
Proc. ACM Program. Lang.
Gilles Barthe, Justin Hsu, Kevin Liao
2020 J jnl
A survey of algorithmic recourse: definitions, formulations, solutions, and prospects.
CoRR
Amir-Hossein Karimi, Gilles Barthe, Bernhard Schölkopf, Isabel Valera
2020 Misc conf
Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification.
INDOCRYPT
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Vincent Laporte, Tiago Oliveira
2020 A* conf
Constant-time foundations for the new spectre era.
PLDI
Sunjay Cauligi, Craig Disselkoen, Klaus von Gleissenthall, Dean M. Tullsen, Deian Stefan, Tamara Rezk, Gilles Barthe
2020 J jnl
Deciding Accuracy of Differential Privacy Schemes.
CoRR
Gilles Barthe, Rohit Chadha, Paul Krogmeier, A. Prasad Sistla, Mahesh Viswanathan
2020 A* conf
Deciding Differential Privacy for Programs with Finite Inputs and Outputs.
LICS
Gilles Barthe, Rohit Chadha, Vishal Jagannath, A. Prasad Sistla, Mahesh Viswanathan
2020 J jnl
Formal verification of a constant-time preserving C compiler.
Proc. ACM Program. Lang.
Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu
2020 — book
Foundations of Probabilistic Programming
Gilles Barthe, Joost-Pieter Katoen, Alexandra Silva
2020 J jnl
High-Assurance Cryptography Software in the Spectre Era.
IACR Cryptol. ePrint Arch.
Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, Tiago Oliveira, Swarn Priya, Tamara Rezk, Peter Schwabe
2020 A conf
Hypothesis Testing Interpretations and Renyi Differential Privacy.
AISTATS
Borja Balle, Gilles Barthe, Marco Gaboardi, Justin Hsu, Tetsuya Sato
2020 J jnl
Improved parallel mask refreshing algorithms: generic solutions with parametrized non-interference and automated optimizations.
J. Cryptogr. Eng.
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub
2020 J jnl
Masking in Fine-Grained Leakage Models: Construction, Implementation and Verification.
IACR Cryptol. ePrint Arch.
Gilles Barthe, Marc Gourjon, Benjamin Grégoire, Maximilian Orlt, Clara Paglialonga, Lars Porth
2020 A conf
Model-Agnostic Counterfactual Explanations for Consequential Decisions.
AISTATS
Amir-Hossein Karimi, Gilles Barthe, Borja Balle, Isabel Valera
2020 A conf
On the Versatility of Open Logical Relations - Continuity, Automatic Differentiation, and a Containment Theorem.
ESOP
Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo
2020 J jnl
On the Versatility of Open Logical Relations: Continuity, Automatic Differentiation, and a Containment Theorem.
CoRR
Gilles Barthe, Raphaëlle Crubillé, Ugo Dal Lago, Francesco Gavazzo
2020 J jnl
PanCast: Listening to Bluetooth Beacons for Epidemic Risk Mitigation.
CoRR
Gilles Barthe, Roberta De Viti, Peter Druschel, Deepak Garg, Manuel Gomez-Rodriguez, Pierfrancesco Ingo, Matthew Lentz, Aastha Mehta, Bernhard Schölkopf
2020 J jnl
Privacy Profiles and Amplification by Subsampling.
J. Priv. Confidentiality
Borja Balle, Gilles Barthe, Marco Gaboardi
2020 — ch.
Probabilistic Couplings from Program Logics.
Foundations of Probabilistic Programming
Gilles Barthe, Justin Hsu
2020 J jnl
Relational proofs for quantum programs.
Proc. ACM Program. Lang.
Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, Li Zhou
2020 J jnl
Scaling Guarantees for Nearest Counterfactual Explanations.
CoRR
Kiarash Mohammadi, Amir-Hossein Karimi, Gilles Barthe, Isabel Valera
2020 J jnl
System-Level Non-interference of Constant-Time Cryptography. Part II: Verified Static Analysis and Stealth Memory.
J. Autom. Reason.
Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, David Pichardie
2020 A* conf
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations.
SP
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub
2020 A* conf
Universal equivalence and majority of probabilistic programs over finite fields.
LICS
Gilles Barthe, Charlie Jacomme, Steve Kremer
2019 A* conf
A Machine-Checked Proof of Security for AWS Key Management Service.
CCS
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran
2019 J jnl
A Machine-Checked Proof of Security for AWS Key Management Service.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran
2019 J jnl
A Probabilistic Separation Logic.
CoRR
Gilles Barthe, Justin Hsu, Kevin Liao
2019 J jnl
A relational logic for higher-order programs.
J. Funct. Program.
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub
2019 A* conf
Approximate Span Liftings: Compositional Semantics for Relaxations of Differential Privacy.
LICS
Tetsuya Sato, Gilles Barthe, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata
2019 J jnl
Automated Analysis of Cryptographic Assumptions in Generic Group Models.
J. Cryptol.
Gilles Barthe, Edvard Fagerholm, Dario Fiore, John C. Mitchell, Andre Scedrov, Benedikt Schmidt
2019 J jnl
Automated Methods for Checking Differential Privacy.
CoRR
Gilles Barthe, Rohit Chadha, Vishal Jagannath, A. Prasad Sistla, Mahesh Viswanathan
2019 A* conf
Bidirectional type checking for relational properties.
PLDI
Ezgi Çiçek, Weihao Qu, Gilles Barthe, Marco Gaboardi, Deepak Garg
2019 J jnl
Coupling Techniques for Reasoning about Quantum Programs.
CoRR
Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, Li Zhou
2019 A* conf
FaCT: a DSL for timing-sensitive computation.
PLDI
Sunjay Cauligi, Gary Soeller, Brian Johannesmeyer, Fraser Brown, Riad S. Wahby, John Renner, Benjamin Grégoire, Gilles Barthe, Ranjit Jhala, Deian Stefan
2019 J jnl
Formal Verification of a Constant-Time Preserving C Compiler.
IACR Cryptol. ePrint Arch.
Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu
2019 J jnl
Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization.
Proc. ACM Program. Lang.
Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Justin Hsu
2019 A* conf
GALACTICS: Gaussian Sampling for Lattice-Based Constant- Time Implementation of Cryptographic Signatures, Revisited.
CCS
Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque, Mélissa Rossi, Mehdi Tibouchi
2019 J jnl
GALACTICS: Gaussian Sampling for Lattice-Based Constant-Time Implementation of Cryptographic Signatures, Revisited.
IACR Cryptol. ePrint Arch.
Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque, Mélissa Rossi, Mehdi Tibouchi
2019 J jnl
Hypothesis Testing Interpretations and Renyi Differential Privacy.
CoRR
Borja Balle, Gilles Barthe, Marco Gaboardi, Justin Hsu, Tetsuya Sato
2019 J jnl
Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs.
J. Autom. Reason.
Patrick Baillot, Gilles Barthe, Ugo Dal Lago
2019 J jnl
Kantorovich Continuity of Probabilistic Programs.
CoRR
Alejandro Aguirre, Gilles Barthe, Justin Hsu, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
2019 J jnl
Machine-Checked Proofs for Cryptographic Standards.
IACR Cryptol. ePrint Arch.
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
2019 A* conf
Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3.
CCS
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
2019 J jnl
Model-Agnostic Counterfactual Explanations for Consequential Decisions.
CoRR
Amir-Hossein Karimi, Gilles Barthe, Borja Balle, Isabel Valera
2019 A* conf
Privacy Amplification by Mixing and Diffusion Mechanisms.
NeurIPS
Borja Balle, Gilles Barthe, Marco Gaboardi, Joseph Geumlek
2019 J jnl
Privacy Amplification by Mixing and Diffusion Mechanisms.
CoRR
Borja Balle, Gilles Barthe, Marco Gaboardi, Joseph Geumlek
2019 J jnl
Program for TPDP 2016.
J. Priv. Confidentiality
Gilles Barthe, Christos Dimitrakakis, Marco Gaboardi, Andreas Haeberlen, Aaron Roth, Aleksandra B. Slavkovic
2019 J jnl
Relational ⋆⋆\star-Liftings for Differential Privacy.
Log. Methods Comput. Sci.
Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub
2019 J jnl
SoK: Computer-Aided Cryptography.
IACR Cryptol. ePrint Arch.
Manuel Barbosa, Gilles Barthe, Karthikeyan Bhargavan, Bruno Blanchet, Cas Cremers, Kevin Liao, Bryan Parno
2019 A conf
Symbolic Methods in Computational Cryptography Proofs.
CSF
Gilles Barthe, Benjamin Grégoire, Charlie Jacomme, Steve Kremer, Pierre-Yves Strub
2019 J jnl
System-Level Non-interference of Constant-Time Cryptography. Part I: Model.
J. Autom. Reason.
Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna
2019 J jnl
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations.
CoRR
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub
2019 J jnl
Towards Constant-Time Foundations for the New Spectre Era.
CoRR
Sunjay Cauligi, Craig Disselkoen, Klaus von Gleissenthall, Deian Stefan, Tamara Rezk, Gilles Barthe
2019 B conf
Verifying Relational Properties using Trace Logic.
FMCAD
Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovács, Matteo Maffei
2019 J jnl
Verifying Relational Properties using Trace Logic.
CoRR
Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovács, Matteo Maffei
2019 — conf
maskVerif: Automated Verification of Higher-Order Masking in Presence of Physical Defaults.
ESORICS (1)
Gilles Barthe, Sonia Belaïd, Gaëtan Cassiers, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert
2018 A* conf
Almost Sure Productivity.
ICALP
Alejandro Aguirre, Gilles Barthe, Justin Hsu, Alexandra Silva
2018 J jnl
Almost Sure Productivity.
CoRR
Alejandro Aguirre, Gilles Barthe, Justin Hsu, Alexandra Silva
2018 A conf
An Assertion-Based Program Logic for Probabilistic Programs.
ESOP
Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2018 J jnl
An Assertion-Based Program Logic for Probabilistic Programs.
CoRR
Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2018 J jnl
Bidirectional Type Checking for Relational Properties.
CoRR
Ezgi Çiçek, Weihao Qu, Gilles Barthe, Marco Gaboardi, Deepak Garg
2018 A conf
Enforcing Ideal-World Leakage Bounds in Real-World Secret Sharing MPC Frameworks.
CSF
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela
2018 J jnl
Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela
2018 J jnl
Facets of Software Doping.
CoRR
Gilles Barthe, Pedro R. D'Argenio, Bernd Finkbeiner, Holger Hermanns
2018 J jnl
Formal verification of higher-order probabilistic programs.
CoRR
Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Justin Hsu
2018 J jnl
Improved Parallel Mask Refreshing Algorithms: Generic Solutions with Parametrized Non-Interference & Automated Optimizations.
IACR Cryptol. ePrint Arch.
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub
2018 — ed.
LPAR-22 Workshop and Short Paper Proceedings, Awassa, Ethiopia, 16-21 November 2018
LPAR (Workshop and Short Papers)
Gilles Barthe, Konstantin Korovin, Stephan Schulz, Martin Suda, Geoff Sutcliffe, Margus Veanes
2018 B ed.
LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Awassa, Ethiopia, 16-21 November 2018
LPAR
Gilles Barthe, Geoff Sutcliffe, Margus Veanes
2018 — conf
Masking the GLP Lattice-Based Signature Scheme at Any Order.
EUROCRYPT (2)
Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque, Benjamin Grégoire, Mélissa Rossi, Mehdi Tibouchi
2018 J jnl
Masking the GLP Lattice-Based Signature Scheme at Any Order.
IACR Cryptol. ePrint Arch.
Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque, Benjamin Grégoire, Mélissa Rossi, Mehdi Tibouchi
2018 J jnl
Monadic refinements for relational cost analysis.
Proc. ACM Program. Lang.
Ivan Radicek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Florian Zuleger
2018 A* conf
Privacy Amplification by Subsampling: Tight Analyses via Couplings and Divergences.
NeurIPS
Borja Balle, Gilles Barthe, Marco Gaboardi
2018 J jnl
Privacy Amplification by Subsampling: Tight Analyses via Couplings and Divergences.
CoRR
Borja Balle, Gilles Barthe, Marco Gaboardi
2018 J jnl
Proving expected sensitivity of probabilistic programs.
Proc. ACM Program. Lang.
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2018 A conf
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus.
ESOP
Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, Deepak Garg
2018 J jnl
Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus.
CoRR
Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, Deepak Garg
2018 A conf
Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic "Constant-Time".
CSF
Gilles Barthe, Benjamin Grégoire, Vincent Laporte
2018 A* conf
Symbolic Proofs for Lattice-Based Cryptography.
CCS
Gilles Barthe, Xiong Fan, Joshua Gancher, Benjamin Grégoire, Charlie Jacomme, Elaine Shi
2018 J jnl
Symbolic Proofs for Lattice-Based Cryptography.
IACR Cryptol. ePrint Arch.
Gilles Barthe, Xiong Fan, Joshua Gancher, Benjamin Grégoire, Charlie Jacomme, Elaine Shi
2018 J jnl
maskVerif: a formal tool for analyzing software and hardware masked implementations.
IACR Cryptol. ePrint Arch.
Gilles Barthe, Sonia Belaïd, Pierre-Alain Fouque, Benjamin Grégoire
2017 A* conf
*-Liftings for Differential Privacy.
ICALP
Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub
2017 J jnl
*-Liftings for Differential Privacy.
CoRR
Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub
2017 A* conf
A Fast and Verified Software Stack for Secure Function Evaluation.
CCS
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira
2017 J jnl
A Fast and Verified Software Stack for Secure Function Evaluation.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira
2017 J jnl
A Note on 'Further Improving Efficiency of Higher-Order Masking Scheme by Decreasing Randomness Complexity'.
IACR Cryptol. ePrint Arch.
Gilles Barthe, François Dupressoir, Benjamin Grégoire
2017 J jnl
A Relational Logic for Higher-Order Programs.
CoRR
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub
2017 J jnl
A relational logic for higher-order programs.
Proc. ACM Program. Lang.
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub
2017 A* conf
Attribute-Based Encryption in the Generic Group Model: Automated Proofs and New Constructions.
CCS
Miguel Ambrona, Gilles Barthe, Romain Gay, Hoeteck Wee
2017 J jnl
Attribute-Based Encryption in the Generic Group Model: Automated Proofs and New Constructions.
IACR Cryptol. ePrint Arch.
Miguel Ambrona, Gilles Barthe, Romain Gay, Hoeteck Wee
2017 A* conf
Coupling proofs are probabilistic product programs.
POPL
Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2017 — conf
Generic Transformations of Predicate Encodings: Constructions and Applications.
CRYPTO (1)
Miguel Ambrona, Gilles Barthe, Benedikt Schmidt
2017 A conf
Is Your Software on Dope? - Formal Analysis of Surreptitiously "enhanced" Programs.
ESOP
Pedro R. D'Argenio, Gilles Barthe, Sebastian Biewer, Bernd Finkbeiner, Holger Hermanns
2017 J jnl
Is your software on dope? Formal analysis of surreptitiously "enhanced" programs.
CoRR
Pedro R. D'Argenio, Gilles Barthe, Sebastian Biewer, Bernd Finkbeiner, Holger Hermanns
2017 A* conf
Jasmin: High-Assurance and High-Speed Cryptography.
CCS
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, Pierre-Yves Strub
2017 — conf
Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model.
EUROCRYPT (1)
Gilles Barthe, François Dupressoir, Sebastian Faust, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub
2017 J jnl
Provably secure compilation of side-channel countermeasures.
IACR Cryptol. ePrint Arch.
Gilles Barthe, Benjamin Grégoire, Vincent Laporte
2017 J jnl
Proving Expected Sensitivity of Probabilistic Programs.
CoRR
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2017 B conf
Proving uniformity and independence by self-composition and coupling.
LPAR
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2017 J jnl
Proving uniformity and independence by self-composition and coupling.
CoRR
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2017 J jnl
Reasoning about Divergences for Relaxations of Differential Privacy.
CoRR
Tetsuya Sato, Gilles Barthe, Marco Gaboardi, Justin Hsu, Shin-ya Katsumata
2017 A conf
Reasoning about Probabilistic Defense Mechanisms against Remote Attacks.
EuroS&P
Martín Ochoa, Sebastian Banescu, Cynthia Disenfeld, Gilles Barthe, Vijay Ganesh
2017 J jnl
Reasoning about Probabilistic Defense Mechanisms against Remote Attacks.
CoRR
Martín Ochoa, Sebastian Banescu, Cynthia Disenfeld, Gilles Barthe, Vijay Ganesh
2017 A* conf
Relational cost analysis.
POPL
Ezgi Çiçek, Gilles Barthe, Marco Gaboardi, Deepak Garg, Jan Hoffmann
2017 A conf
Verified Translation Validation of Static Analyses.
CSF
Gilles Barthe, Sandrine Blazy, Vincent Laporte, David Pichardie, Alix Trieu
2016 A* conf
A Program Logic for Union Bounds.
ICALP
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2016 J jnl
A program logic for union bounds.
CoRR
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2016 A* conf
Advanced Probabilistic Couplings for Differential Privacy.
CCS
Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2016 J jnl
Advanced Probabilistic Couplings for Differential Privacy.
CoRR
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2016 — conf
Automated Unbounded Analysis of Cryptographic Constructions in the Generic Group Model.
EUROCRYPT (2)
Miguel Ambrona, Gilles Barthe, Benedikt Schmidt
2016 J jnl
Automated Unbounded Analysis of Cryptographic Constructions in the Generic Group Model.
IACR Cryptol. ePrint Arch.
Miguel Ambrona, Gilles Barthe, Benedikt Schmidt
2016 — conf
Computer-Aided Verification for Mechanism Design.
WINE
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub
2016 J jnl
Coupling proofs are probabilistic product programs.
CoRR
Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2016 A* conf
Differentially Private Bayesian Programming.
CCS
Gilles Barthe, Gian Pietro Farina, Marco Gaboardi, Emilio Jesús Gallego Arias, Andy Gordon, Justin Hsu, Pierre-Yves Strub
2016 J jnl
Differentially Private Bayesian Programming.
CoRR
Gilles Barthe, Gian Pietro Farina, Marco Gaboardi, Emilio Jesús Gallego Arias, Andy Gordon, Justin Hsu, Pierre-Yves Strub
2016 — conf
Facets of Software Doping.
ISoLA (2)
Gilles Barthe, Pedro R. D'Argenio, Bernd Finkbeiner, Holger Hermanns
2016 J jnl
Generic Transformations of Predicate Encodings: Constructions and Applications.
IACR Cryptol. ePrint Arch.
Miguel Ambrona, Gilles Barthe, Benedikt Schmidt
2016 J jnl
Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model.
IACR Cryptol. ePrint Arch.
Gilles Barthe, François Dupressoir, Sebastian Faust, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub
2016 J jnl
Product programs and relational program logics.
J. Log. Algebraic Methods Program.
Gilles Barthe, Juan Manuel Crespo, César Kunz
2016 J jnl
Programming language techniques for differential privacy.
ACM SIGLOG News
Gilles Barthe, Marco Gaboardi, Justin Hsu, Benjamin C. Pierce
2016 A* conf
Proving Differential Privacy via Probabilistic Couplings.
LICS
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2016 J jnl
Proving Differential Privacy via Probabilistic Couplings.
CoRR
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2016 — ed.
Security and Trust Management - 12th International Workshop, STM 2016, Heraklion, Crete, Greece, September 26-27, 2016, Proceedings
STM
Gilles Barthe, Evangelos P. Markatos, Pierangela Samarati
2016 A* conf
Strong Non-Interference and Type-Directed Higher-Order Masking.
CCS
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub, Rébecca Zucchini
2016 J jnl
Strongly-optimal structure preserving signatures from Type II pairings: synthesis and lower bounds.
IET Inf. Secur.
Gilles Barthe, Edvard Fagerholm, Dario Fiore, Andre Scedrov, Benedikt Schmidt, Mehdi Tibouchi
2016 — conf
Synthesizing Probabilistic Invariants via Doob's Decomposition.
CAV (1)
Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti, Justin Hsu
2016 J jnl
Synthesizing Probabilistic Invariants via Doob's Decomposition.
CoRR
Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti, Justin Hsu
2016 A* conf
Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC.
FSE
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir
2016 A* conf
Verifying Constant-Time Implementations.
USENIX Security Symposium
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Michael Emmi
2015 A* conf
Automated Proofs of Pairing-Based Cryptography.
CCS
Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt
2015 J jnl
Challenges and Trends in Probabilistic Programming (Dagstuhl Seminar 15181).
Dagstuhl Reports
Gilles Barthe, Andrew D. Gordon, Joost-Pieter Katoen, Annabelle McIver
2015 J jnl
Compositional Verification of Higher-Order Masking: Application to a Verifying Masking Compiler.
IACR Cryptol. ePrint Arch.
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire
2015 J jnl
Computer-aided verification in mechanism design.
CoRR
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub
2015 J jnl
High-Assurance Cryptography: Cryptographic Software We Can Trust.
IEEE Secur. Priv.
Gilles Barthe
2015 A* conf
Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy.
POPL
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub
2015 B conf
Implicit Computational Complexity of Subrecursive Definitions and Applications to Cryptographic Proofs.
LPAR
Patrick Baillot, Gilles Barthe, Ugo Dal Lago
2015 — conf
Mind the Gap: Modular Machine-Checked Proofs of One-Round Key Exchange Protocols.
EUROCRYPT (2)
Gilles Barthe, Juan Manuel Crespo, Yassine Lakhnech, Benedikt Schmidt
2015 J jnl
Mind the Gap: Modular Machine-checked Proofs of One-Round Key Exchange Protocols.
IACR Cryptol. ePrint Arch.
Gilles Barthe, Juan Manuel Crespo, Yassine Lakhnech, Benedikt Schmidt
2015 B conf
Relational Reasoning via Probabilistic Coupling.
LPAR
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub
2015 J jnl
Relational reasoning via probabilistic coupling.
CoRR
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub
2015 J jnl
SEFM: software engineering and formal methods.
Softw. Syst. Model.
Gilles Barthe, Alberto Pardo, Gerardo Schneider
2015 — conf
Strongly-Optimal Structure Preserving Signatures from Type II Pairings: Synthesis and Lower Bounds.
Public Key Cryptography
Gilles Barthe, Edvard Fagerholm, Dario Fiore, Andre Scedrov, Benedikt Schmidt, Mehdi Tibouchi
2015 J jnl
Strongly-Optimal Structure Preserving Signatures from Type II Pairings: Synthesis and Lower Bounds.
IACR Cryptol. ePrint Arch.
Gilles Barthe, Edvard Fagerholm, Dario Fiore, Andre Scedrov, Benedikt Schmidt, Mehdi Tibouchi
2015 J jnl
Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir
2015 — conf
Verified Proofs of Higher-Order Masking.
EUROCRYPT (1)
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub
2015 J jnl
Verified Proofs of Higher-Order Masking.
IACR Cryptol. ePrint Arch.
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub
2014 — conf
Automated Analysis of Cryptographic Assumptions in Generic Group Models.
CRYPTO (1)
Gilles Barthe, Edvard Fagerholm, Dario Fiore, John C. Mitchell, Andre Scedrov, Benedikt Schmidt
2014 J jnl
Automated Analysis of Cryptographic Assumptions in Generic Group Models.
IACR Cryptol. ePrint Arch.
Gilles Barthe, Edvard Fagerholm, Dario Fiore, John C. Mitchell, Andre Scedrov, Benedikt Schmidt
2014 A conf
Certified Synthesis of Efficient Batch Verifiers.
CSF
Joseph A. Akinyele, Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt, Pierre-Yves Strub
2014 J jnl
Formal Verification of an SSA-Based Middle-End for CompCert.
ACM Trans. Program. Lang. Syst.
Gilles Barthe, Delphine Demange, David Pichardie
2014 J jnl
Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy.
CoRR
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub
2014 — conf
Leakage Resilience against Concurrent Cache Attacks.
POST
Gilles Barthe, Boris Köpf, Laurent Mauborgne, Martín Ochoa
2014 J jnl
Making RSA-PSS Provably Secure Against Non-Random Faults.
IACR Cryptol. ePrint Arch.
Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Mehdi Tibouchi, Jean-Christophe Zapalowicz
2014 A conf
Making RSA-PSS Provably Secure against Non-random Faults.
CHES
Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Mehdi Tibouchi, Jean-Christophe Zapalowicz
2014 A* conf
Probabilistic relational verification for cryptographic implementations.
POPL
Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella-Béguelin
2014 A conf
Proving Differential Privacy in Hoare Logic.
CSF
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz, Pierre-Yves Strub
2014 J jnl
Proving differential privacy in Hoare logic.
CoRR
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz, Pierre-Yves Strub
2014 A* conf
Synthesis of Fault Attacks on Cryptographic Implementations.
CCS
Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Jean-Christophe Zapalowicz
2014 J jnl
Synthesis of Fault Attacks on Cryptographic Implementations.
IACR Cryptol. ePrint Arch.
Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Jean-Christophe Zapalowicz
2014 A* conf
System-level Non-interference for Constant-time Cryptography.
CCS
Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Daniel Luna, David Pichardie
2014 J jnl
System-level non-interference for constant-time cryptography.
IACR Cryptol. ePrint Arch.
Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna, David Pichardie
2014 J jnl
The Synergy Between Programming Languages and Cryptography (Dagstuhl Seminar 14492).
Dagstuhl Reports
Gilles Barthe, Michael Hicks, Florian Kerschbaum, Dominique Unruh
2014 J jnl
Verified Implementations for Secure and Verifiable Computation.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Guillaume Davy, François Dupressoir, Benjamin Grégoire, Pierre-Yves Strub
2013 J jnl
A certified lightweight non-interference Java bytecode verifier.
Math. Struct. Comput. Sci.
Gilles Barthe, David Pichardie, Tamara Rezk
2013 Misc conf
Beyond 2-Safety: Asymmetric Product Programs for Relational Program Verification.
LFCS
Gilles Barthe, Juan Manuel Crespo, César Kunz
2013 — conf
Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic Programs.
ICALP (2)
Gilles Barthe, Federico Olmedo
2013 A* conf
Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations.
CCS
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir
2013 J jnl
Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir
2013 — conf
Computer-Aided Security Proofs.
QEST
Gilles Barthe
2013 — conf
EasyCrypt: A Tutorial.
FOSAD
Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, Pierre-Yves Strub
2013 — conf
Formally Verified Implementation of an Idealized Model of Virtualization.
TYPES
Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Jesús Mauricio Chimento, Carlos Luna
2013 B conf
From relational verification to SIMD loop synthesis.
PPoPP
Gilles Barthe, Juan Manuel Crespo, Sumit Gulwani, César Kunz, Mark Marron
2013 A* conf
Fully automated analysis of padding-based encryption in the computational model.
CCS
Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Benedikt Schmidt, Santiago Zanella-Béguelin
2013 J jnl
Probabilistic Relational Reasoning for Differential Privacy.
ACM Trans. Program. Lang. Syst.
Gilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella-Béguelin
2013 A conf
Verified Computational Differential Privacy with Applications to Smart Metering.
CSF
Gilles Barthe, George Danezis, Benjamin Grégoire, César Kunz, Santiago Zanella-Béguelin
2013 J jnl
Verified indifferentiable hashing into elliptic curves.
J. Comput. Secur.
Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella-Béguelin
2012 A conf
A Formally Verified SSA-Based Middle-End - Static Single Assignment Meets CompCert.
ESOP
Gilles Barthe, Delphine Demange, David Pichardie
2012 J jnl
Automated Analysis and Synthesis of Padding-Based Encryption Schemes.
IACR Cryptol. ePrint Arch.
Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella-Béguelin
2012 B conf
Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs.
CPP
Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella-Béguelin
2012 A conf
Cache-Leakage Resilient OS Isolation in an Idealized Model of Virtualization.
CSF
Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna
2012 B conf
Computer-Aided Cryptographic Proofs.
ITP
Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella-Béguelin
2012 B conf
Computer-Aided Cryptographic Proofs.
SAS
Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
2012 — ed.
Engineering Secure Software and Systems - 4th International Symposium, ESSoS 2012, Eindhoven, The Netherlands, February, 16-17, 2012. Proceedings
ESSoS
Gilles Barthe, Benjamin Livshits, Riccardo Scandariato
2012 — ed.
Formal Aspects of Security and Trust - 8th International Workshop, FAST 2011, Leuven, Belgium, September 12-14, 2011. Revised Selected Papers
Formal Aspects in Security and Trust
Gilles Barthe, Anupam Datta, Sandro Etalle
2012 J jnl
Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe, Stephan Krenn, Santiago Zanella-Béguelin
2012 A* conf
Full proof cryptography: verifiable compilation of efficient zero-knowledge protocols.
CCS
José Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe, Stephan Krenn, Santiago Zanella-Béguelin
2012 J jnl
Preface.
J. Comput. Secur.
Gilles Barthe, Jorge Cuéllar, Javier López, Alexander Pretschner
2012 B conf
Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs.
MPC
Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
2012 A* conf
Probabilistic relational reasoning for differential privacy.
POPL
Gilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella-Béguelin
2012 — conf
Secure Multi-Execution through Static Program Transformation.
FMOODS/FORTE
Gilles Barthe, Juan Manuel Crespo, Dominique Devriese, Frank Piessens, Exequiel Rivas
2012 — conf
Verified Indifferentiable Hashing into Elliptic Curves.
POST
Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella-Béguelin
2012 A conf
Verified Security of Merkle-Damgård.
CSF
Michael Backes, Gilles Barthe, Matthias Berg, Benjamin Grégoire, César Kunz, Malte Skoruppa, Santiago Zanella-Béguelin
2012 J jnl
Verified Security of Redundancy-Free Encryption from Rabin and RSA.
IACR Cryptol. ePrint Arch.
Gilles Barthe, David Pointcheval, Santiago Zanella-Béguelin
2012 A* conf
Verified security of redundancy-free encryption from Rabin and RSA.
CCS
Gilles Barthe, David Pointcheval, Santiago Zanella-Béguelin
2011 — conf
A Computational Indistinguishability Logic for the Bounded Storage Model.
FPS
Gilles Barthe, Mathilde Duclos, Yassine Lakhnech
2011 J jnl
An Abstract Model of Certificate Translation.
ACM Trans. Program. Lang. Syst.
Gilles Barthe, César Kunz
2011 B conf
Beyond Provable Security Verifiable IND-CCA Security of OAEP.
CT-RSA
Gilles Barthe, Benjamin Grégoire, Yassine Lakhnech, Santiago Zanella-Béguelin
2011 A* conf
Computer-Aided Security Proofs for the Working Cryptographer.
CRYPTO
Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella-Béguelin
2011 B conf
Formally Verifying Isolation and Availability in an Idealized Model of Virtualization.
FM
Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Luna
2011 A conf
Information-Theoretic Bounds for Differentially Private Mechanisms.
CSF
Gilles Barthe, Boris Köpf
2011 J jnl
Information-theoretic Bounds for Differentially Private Mechanisms.
IACR Cryptol. ePrint Arch.
Gilles Barthe, Boris Köpf
2011 A ed.
Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings
ESOP
Gilles Barthe
2011 B conf
Relational Verification Using Product Programs.
FM
Gilles Barthe, Juan Manuel Crespo, César Kunz
2011 J jnl
Secure information flow by self-composition.
Math. Struct. Comput. Sci.
Gilles Barthe, Pedro R. D'Argenio, Tamara Rezk
2011 — ed.
Security and Trust Management - 6th International Workshop, STM 2010, Athens, Greece, September 23-24, 2010, Revised Selected Papers
STM
Jorge Cuéllar, Gilles Barthe, Alexander Pretschner, Javier López
2011 B ed.
Software Engineering and Formal Methods - 9th International Conference, SEFM 2011, Montevideo, Uruguay, November 14-18, 2011. Proceedings
SEFM
Gilles Barthe, Alberto Pardo, Gerardo Schneider
2011 — conf
Static Enforcement of Information Flow Policies for a Concurrent JVM-like Language.
TGC
Gilles Barthe, Exequiel Rivas
2011 C conf
Verifiable Security of Boneh-Franklin Identity-Based Encryption.
ProvSec
Gilles Barthe, Federico Olmedo, Santiago Zanella-Béguelin
2010 Misc conf
A Functional Framework for Result Checking.
FLOPS
Gilles Barthe, Pablo Buiras, César Kunz
2010 A conf
A Machine-Checked Formalization of Sigma-Protocols.
CSF
Gilles Barthe, Daniel Hedin, Santiago Zanella-Béguelin, Benjamin Grégoire, Sylvain Heraud
2010 A* conf
Computational indistinguishability logic.
CCS
Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech
2010 — conf
On the Equality of Probabilistic Terms.
LPAR (Dakar)
Gilles Barthe, Marion Daubignard, Bruce M. Kapron, Yassine Lakhnech, Vincent Laporte
2010 — conf
Perspectives in Certificate Translation.
TGC
Gilles Barthe, César Kunz
2010 B conf
Programming Language Techniques for Cryptographic Proofs.
ITP
Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
2010 A conf
Robustness Guarantees for Anonymity.
CSF
Gilles Barthe, Alejandro Hevia, Zhengqin Luo, Tamara Rezk, Bogdan Warinschi
2010 J jnl
Security of multithreaded programs by compilation.
ACM Trans. Inf. Syst. Secur.
Gilles Barthe, Tamara Rezk, Alejandro Russo, Andrei Sabelfeld
2010 B ed.
Verification, Model Checking, and Abstract Interpretation, 11th International Conference, VMCAI 2010, Madrid, Spain, January 17-19, 2010. Proceedings
VMCAI
Gilles Barthe, Manuel V. Hermenegildo
2009 J jnl
Certificate translation for optimizing compilers.
ACM Trans. Program. Lang. Syst.
Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk
2009 A* conf
Formal certification of code-based cryptographic proofs.
POPL
Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
2009 A* conf
Formally Certifying the Security of Digital Signature Schemes.
SP
Santiago Zanella-Béguelin, Gilles Barthe, Benjamin Grégoire, Federico Olmedo
2009 — ed.
Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures
FOSAD
Alessandro Aldini, Gilles Barthe, Roberto Gorrieri
2009 C conf
Implementing a Direct Method for Certificate Translation.
ICFEM
Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, César Kunz, Anne Pacalet
2008 — conf
A Tutorial on Type-Based Termination.
LerNet ALFA Summer School
Gilles Barthe, Benjamin Grégoire, Colin Riba
2008 — conf
An Introduction to Certificate Translation.
FOSAD
Gilles Barthe, César Kunz
2008 A conf
Certificate Translation in Abstract Interpretation.
ESOP
Gilles Barthe, César Kunz
2008 — conf
Certificate Translation.
VERIFY
Gilles Barthe
2008 — conf
Certificate translation for specification-preserving advices.
FOAL
Gilles Barthe, César Kunz
2008 B conf
Certified Reasoning in Memory Hierarchies.
APLAS
Gilles Barthe, César Kunz, Jorge luis Sacchini
2008 — conf
Formal Certification of ElGamal Encryption.
Formal Aspects in Security and Trust
Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella-Béguelin
2008 — ed.
Formal Methods for Open Object-Based Distributed Systems, 10th IFIP WG 6.1 International Conference, FMOODS 2008, Oslo, Norway, June 4-6, 2008, Proceedings
FMOODS
Gilles Barthe, Frank S. de Boer
2008 A conf
Preservation of Proof Obligations from Java to the Java Virtual Machine.
IJCAR
Gilles Barthe, Benjamin Grégoire, Mariela Pavlova
2008 B conf
Preservation of Proof Pbligations for Hybrid Verification Methods.
SEFM
Gilles Barthe, César Kunz, David Pichardie, Julián Samborski-Forlese
2008 A conf
Tractable Enforcement of Declassification Policies.
CSF
Gilles Barthe, Salvador Cavadini, Tamara Rezk
2008 — ed.
Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers
TGC
Gilles Barthe, Cédric Fournet
2008 B conf
Type-Based Termination with Sized Products.
CSL
Gilles Barthe, Benjamin Grégoire, Colin Riba
2007 — conf
07091 Abstracts Collection - Mobility, Ubiquity and Security.
Mobility, Ubiquity and Security
Gilles Barthe, Heiko Mantel, Peter Müller, Andrew C. Myers, Andrei Sabelfeld
2007 — conf
07091 Executive Summary - Mobility, Ubiquity and Security.
Mobility, Ubiquity and Security
Gilles Barthe, Heiko Mantel, Peter Müller, Andrew C. Myers, Andrei Sabelfeld
2007 A conf
A Certified Lightweight Non-interference Java Bytecode Verifier.
ESOP
Gilles Barthe, David Pichardie, Tamara Rezk
2007 — ed.
Mobility, Ubiquity and Security, 25.02. - 02.03.2007
Mobility, Ubiquity and Security
Gilles Barthe, Heiko Mantel, Peter Müller, Andrew C. Myers, Andrei Sabelfeld
2007 J jnl
Secure information flow for a concurrent language with scheduling.
J. Comput. Secur.
Gilles Barthe, Leonor Prensa Nieto
2007 A conf
Security of Multithreaded Programs by Compilation.
ESORICS
Gilles Barthe, Tamara Rezk, Alejandro Russo, Andrei Sabelfeld
2007 J jnl
Security types preserving compilation.
Comput. Lang. Syst. Struct.
Gilles Barthe, Tamara Rezk, Amitabh Basu
2007 — conf
The MOBIUS Proof Carrying Code Infrastructure.
FMCO
Gilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas P. Jensen, David Pichardie
2006 B conf
CIC[^( )]: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions.
LPAR
Gilles Barthe, Benjamin Grégoire, Fernando Pastawski
2006 B conf
Certificate Translation for Optimizing Compilers.
SAS
Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk
2006 — ed.
Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, Second International Workshop, CASSIS 2005, Nice, France, March 8-11, 2005, Revised Selected Papers
CASSIS
Gilles Barthe, Benjamin Grégoire, Marieke Huisman, Jean-Louis Lanet
2006 Misc conf
Defining and Reasoning About Recursive Functions: A Practical Tool for the Coq Proof Assistant.
FLOPS
Gilles Barthe, Julien Forest, David Pichardie, Vlad Rusu
2006 — conf
Deriving an Information Flow Checker and Certifying Compiler for Java.
S&P
Gilles Barthe, Tamara Rezk, David A. Naumann
2006 — conf
JACK - A Tool for Validation of Security and Behaviour of Java Applications.
FMCO
Gilles Barthe, Lilian Burdy, Julien Charles, Benjamin Grégoire, Marieke Huisman, Jean-Louis Lanet, Mariela Pavlova, Antoine Requet
2006 — conf
MOBIUS: Mobility, Ubiquity, Security.
TGC
Gilles Barthe, Lennart Beringer, Pierre Crégut, Benjamin Grégoire, Martin Hofmann, Peter Müller, Erik Poll, Germán Puebla, Ian Stark, Eric Vétillard
2006 J jnl
Remarks on the equational theory of non-normalizing pure type systems.
J. Funct. Program.
Gilles Barthe, Thierry Coquand
2005 J jnl
A computational view of implicit coercions in type theory.
Math. Struct. Comput. Sci.
Gilles Barthe
2005 — ed.
Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, International Workshop, CASSIS 2004, Marseille, France, March 10-14, 2004, Revised Selected Papers
CASSIS
Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet, Traian Muntean
2005 — conf
Formal Methods for Smartcard Security.
FOSAD
Gilles Barthe, Guillaume Dufay
2005 — conf
Non-interference for a JVM-like language.
TLDI
Gilles Barthe, Tamara Rezk
2005 — conf
Practical Inference for Type-Based Termination in a Polymorphic Setting.
TLCA
Gilles Barthe, Benjamin Grégoire, Fernando Pastawski
2005 B conf
Precise Analysis of Memory Consumption using Program Logics.
SEFM
Gilles Barthe, Mariela Pavlova, Gerardo Schneider
2005 — conf
Preventing Timing Leaks Through Transactional Branching Instructions.
QAPL
Gilles Barthe, Tamara Rezk, Martijn Warnier
2005 — conf
Proof Obligations Preserving Compilation.
Formal Aspects in Security and Trust
Gilles Barthe, Tamara Rezk, Ando Saabas
2005 J jnl
Tool-Assisted Specification and Verification of Typed Low-Level Languages.
J. Autom. Reason.
Gilles Barthe, Pierre Courtieu, Guillaume Dufay, Simão Melo de Sousa
2004 A conf
A Machine-Checked Formalization of the Generic Model and the Random Oracle Model.
IJCAR
Gilles Barthe, Jan Cederquist, Sabrina Tarento
2004 — conf
A Machine-Checked Formalization of the Random Oracle Model.
TYPES
Gilles Barthe, Sabrina Tarento
2004 B conf
A Tool-Assisted Framework for Certified Bytecode Verification.
FASE
Gilles Barthe, Guillaume Dufay
2004 C conf
Enforcing High-Level Security Properties for Applets.
CARDIS
Mariela Pavlova, Gilles Barthe, Lilian Burdy, Marieke Huisman, Jean-Louis Lanet
2004 — conf
Formally verifying information flow type systems for concurrent and thread systems.
FMSE
Gilles Barthe, Leonor Prensa Nieto
2004 J jnl
Introduction to the Special Issue on Dependent Type Theory Meets Practical Programming.
J. Funct. Program.
Gilles Barthe, Peter Dybjer, Peter Thiemann
2004 — conf
Secure Information Flow by Self-Composition.
CSFW
Gilles Barthe, Pedro R. D'Argenio, Tamara Rezk
2004 B conf
Security Types Preserving Compilation: (Extended Abstract).
VMCAI
Gilles Barthe, Amitabh Basu, Tamara Rezk
2004 J jnl
Type-based termination of recursive definitions.
Math. Struct. Comput. Sci.
Gilles Barthe, Maria João Frade, Eduardo Giménez, Luís Pinto, Tarmo Uustalu
2003 — ed.
International Workshop in Types in Programming, TIP@MPC 2002, Dagstuhl, Germany, July 8, 2002
TIP@MPC
Gilles Barthe, Peter Thiemann
2003 A* conf
Pure patterns type systems.
POPL
Gilles Barthe, Horatiu Cirstea, Claude Kirchner, Luigi Liquori
2003 J jnl
Setoids in type theory.
J. Funct. Program.
Gilles Barthe, Venanzio Capretta, Olivier Pons
2003 — conf
Validation of the JavaCard Platform with Implicit Induction Techniques.
RTA
Gilles Barthe, Sorin Stratulat
2002 B conf
A Formal Correspondence between Offensive and Defensive JavaCard Virtual Machines.
VMCAI
Gilles Barthe, Guillaume Dufay, Line Jakubiec, Simão Melo de Sousa
2002 — ed.
Applied Semantics, International Summer School, APPSEM 2000, Caminha, Portugal, September 9-15, 2000, Advanced Lectures
APPSEM
Gilles Barthe, Peter Dybjer, Luís Pinto, João Saraiva
2002 C conf
CPS translating inductive and coinductive types.
PEPM
Gilles Barthe, Tarmo Uustalu
2002 B conf
Compositional Verification of Secure Applet Interactions.
FASE
Gilles Barthe, Dilian Gurov, Marieke Huisman
2002 — conf
Efficient Reasoning about Executable Specifications in Coq.
TPHOLs
Gilles Barthe, Pierre Courtieu
2002 — conf
Preface.
TIP@MPC
Gilles Barthe, Peter Thiemann
2002 — conf
Tool-Assisted Specification and Verification of the JavaCard Platform.
AMAST
Gilles Barthe, Pierre Courtieu, Guillaume Dufay, Simão Melo de Sousa
2001 A conf
A Formal Executable Semantics of the JavaCard Platform.
ESOP
Gilles Barthe, Guillaume Dufay, Line Jakubiec, Bernard P. Serpette, Simão Melo de Sousa
2001 J jnl
An induction principle for pure type systems.
Theor. Comput. Sci.
Gilles Barthe, John Hatcliff, Morten Heine Sørensen
2001 — conf
Jakarta: A Toolset for Reasoning about JavaCard.
E-smart
Gilles Barthe, Guillaume Dufay, Marieke Huisman, Simão Melo de Sousa
2001 — conf
Tipos principales y cierre semi-completo para sistemas de tipos puros extendidos (trabajo en desarrollo).
APPIA-GULP-PRODE
Gilles Barthe, Blas C. Ruiz Jiménez
2001 B conf
Type Isomorphisms and Proof Reuse in Dependent Type Theory.
FoSSaCS
Gilles Barthe, Olivier Pons
2001 J jnl
Weak normalization implies strong normalization in a class of non-dependent pure type systems.
Theor. Comput. Sci.
Gilles Barthe, John Hatcliff, Morten Heine Sørensen
2000 — conf
An Introduction to Dependent Type Theory.
APPSEM
Gilles Barthe, Thierry Coquand
2000 B conf
Constructor Subtyping in the Calculus of Inductive Constructions.
FoSSaCS
Gilles Barthe, Femke van Raamsdonk
2000 J jnl
Domain-free pure type systems.
J. Funct. Program.
Gilles Barthe, Morten Heine Sørensen
2000 B conf
Static Reduction Analysis for Imperative Object Oriented Languages.
LPAR
Gilles Barthe, Bernard P. Serpette
1999 J jnl
CPS Translations and Applications: The Cube and Beyond.
High. Order Symb. Comput.
Gilles Barthe, John Hatcliff, Morten Heine Sørensen
1999 A conf
Constructor Subtyping.
ESOP
Gilles Barthe, Maria João Frade
1999 B conf
Expanding the Cube.
FoSSaCS
Gilles Barthe
1999 J jnl
Order-Sorted Inductive Types.
Inf. Comput.
Gilles Barthe
1999 — conf
Partial Evaluation and Non-interference for Object Calculi.
Fuji International Symposium on Functional and Logic Programming
Gilles Barthe, Bernard P. Serpette
1999 J jnl
Type-checking injective pure type systems.
J. Funct. Program.
Gilles Barthe
1998 B conf
Existence and Uniqueness of Normal Forms in Pure Type Systems with betaeta-Conversion.
CSL
Gilles Barthe
1998 A* conf
The Relevance of Proof-Irrelevance.
ICALP
Gilles Barthe
1998 B conf
The Semi-Full Closure of Pure Type Systems.
MFCS
Gilles Barthe
1997 B conf
A notion of classical pure type system.
MFPS
Gilles Barthe, John Hatcliff, Morten Heine Sørensen
1997 Misc conf
Domain-Free Pure Type Systems.
LFCS
Gilles Barthe, Morten Heine Sørensen
1997 — conf
Explicit Substitutions for the Lambda-Calculus.
ALP/HOA
Gilles Barthe, Fairouz Kamareddine, Alejandro Ríos
1997 — conf
Monadic Type Systems: Pure Type Systems for Impure Settings.
HOOTS
Gilles Barthe, John Hatcliff, Peter Thiemann
1997 — conf
Reflections on Reflections.
PLILP
Gilles Barthe, John Hatcliff, Morten Heine Sørensen
1997 — conf
Termination of Algebraic Type Systems: The Syntactic Approach.
ALP/HOA
Gilles Barthe, Femke van Raamsdonk
1996 B conf
On the Subject Reduction Property for Algebraic Type Systems.
CSL
Gilles Barthe, Paul-André Melliès
1996 — conf
Towards Lean Proof Checking.
DISCO
Gilles Barthe, Hugo Elbers
1995 B conf
A Simple Abstract Semantics for Equational Theories.
FCT
Gilles Barthe
1995 — conf
A Two-Level Approach Towards Lean Proof-Checking.
TYPES
Gilles Barthe, Mark Ruys, Henk Barendregt
1995 B conf
Congruence Types.
CSL
Gilles Barthe, Herman Geuvers
1995 — conf
Extensions of Pure Type Systems.
TLCA
Gilles Barthe
1995 — conf
Implicit Coercions in Type Systems.
TYPES
Gilles Barthe
1995 — conf
Modular Properties of Algebraic Type Systems.
HOA
Gilles Barthe, Herman Geuvers