ESPITAU , Thomas

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 program sensitivity for probabilistic programs-expected sensitivity-that averages a distance function over a probabilistic coupling of two output distributions from two...

Proof by coupling is a classical proof technique for establishing probabilistic properties of two probabilistic processes, like stochastic dominance and rapid mixing of Markov chains. More recently, couplings have been investigated as a useful abstraction for formal reasoning about relational properties of probabilistic programs, in particular...

Probabilistic coupling is a powerful tool for analyzing prob-abilistic processes. Roughly, coupling two processes requires finding an appropriate witness process that characterizes both processes in the same probability space. Applications of coupling include reasoning about convergence of distributions, and stochastic dominance—a probabilistic...

Research on deductive verification of probabilistic programs has considered expectation-based logics, where pre-and post-conditions are real-valued functions on states, and assertion-based logics, where pre-and post-conditions are boolean predicates on state distributions. Both approaches have developed over nearly four decades, but they have...

Recently, numerous physical attacks have been demonstrated against lattice-based schemes, often exploiting their unique properties such as the reliance on Gaussian distributions, rejection sampling and FFT-based polynomial multiplication. As the call for concrete implementations and deployment of postquantum cryptography becomes more pressing,...