Vous pouvez vous abonner à nos annonces de séminaires
http://gallium.inria.fr/seminaires/
S E M I N A I R E
__
/ _` _ / / o
/ ) __) / / / / / /\/|
(___/ (_/ (_ (_ / (__/ / |
I N R I A - Rocquencourt
Amphi Turing du bâtiment 1
Lundi 17 novembre, 10h30
---------------------------
Emilio Jesús Gallego Arias
---------------------------
CRI, Mines ParisTech
=========================================
Approximate Relational Refinement Types
with Applications to Verification of
Differential Privacy and Mechanism Design
=========================================
In software verification, properties over two arbitrary runs of a
program are pervasive. The class of "2-properties" or "relational
properties" is known to capture many definitions of interest.
I will present a recent draft [1] introducing a relational
refinement type system (HOARe2) for the verification of
probabilistic relational properties.
We have applied the system to two case studies, Differential
Privacy and Mechanism Design, automatically verifying over 12
state of the art algorithms.
A (probabilistic) algorithm is differentially private if given two
adjacent inputs, the distance on the output probability
distributions is bounded.
Differential Privacy has gathered wide interest in the privacy,
theory and data-analysis community, and it can be understood as a
privacy promise: "Whether we use your data or not, a DP analysis
will be approximately the same".
Mechanism Design is the study of algorithm design in which the
inputs to the algorithm are controlled by strategic agents, who
must be incentivized to faithfully report them.
A particular property of interest is truthfulness: An agent
revenue will be maximal if and only if she tells the truth to the
mechanism.
[1] http://arxiv.org/abs/1407.6845
Joint work with Gilles Barthe, Marco Gaboardi, Justin Hsu, Aaron
Roth and Pierre-Yves Strub.
Short Bio: Emilio got a PhD from the Technical University of Madrid on
categorical and relational semantics for constraint logic
programming; was a post doc in the privacy group of the
University of Pennsylvania for two years; and now he is a
postdoctoral researcher at CRI Mines ParisTech working on the
formal semantics and implementation of Faust, a DSL for
digital signal and audio processing.