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.