Who: Gilles Barthe (IMDEA)\
When: 13:30, May 31 \
Where: room EDIT 8103\
Title: {{ page.title }}
Abstract:\
Differential privacy is a statistical notion of privacy which achieves
compelling trade-offs between input privacy and accuracy (of outputs).
Differential privacy is also an attractive target for verification:
despite their apparent simplicity, recently proposed algorithms have
intricate privacy and accuracy proofs. We present two program logics
for reasoning about privacy and accuracy properties of probabilistic
computations. The accuracy logic captures reasoning about the union
bound, a simple but effective tool from probablility theory, whereas
the privacy logic captures fine-grained reasoning about probabilistic
couplings, a powerful tool for studying Markov chains. We illustrate
the strengths of our program logics with novel and elegant proofs of
challenging examples from differential privacy.
{: .t60 } {% include list-posts tag=‘csstalk’%}