98 citations · 206 across the 5 of their papers we have counts for
8 papers
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe +5
We develop a new approach for building cryptographic implementations. Our approach goes the last mile and delivers assembly code that is provably functionally correct, protected ag…
An Assertion-Based Program Logic for Probabilistic Programs
Gilles Barthe, Thomas Espitau, Marco Gaboardi +3
Research on deductive verification of probabilistic programs has considered expectation-based logics, where pre- and post-conditions are real-valued functions on states, and assert…
Proving Expected Sensitivity of Probabilistic Programs
Gilles Barthe, Thomas Espitau, Benjamin Grégoire +2
Program sensitivity, also known as Lipschitz continuity, describes how small changes in a program's input lead to bounded changes in the output. We propose an average notion of pro…
Proving uniformity and independence by self-composition and coupling
Gilles Barthe, Thomas Espitau, Benjamin Grégoire +2
Proof by coupling is a classical proof technique for establishing probabilistic properties of two probabilistic processes, like stochastic dominance and rapid mixing of Markov chai…
Coupling proofs are probabilistic product programs
Gilles Barthe, Benjamin Grégoire, Justin Hsu +1
Couplings are a powerful mathematical tool for reasoning about pairs of probabilistic processes. Recent developments in formal verification identify a close connection between coup…
A program logic for union bounds
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire +2
We propose a probabilistic Hoare logic aHL based on the union bound, a tool from basic probability theory. While the union bound is simple, it is an extremely common tool for analy…