**16 December 2016**, 9:00: Computer-Aided Verification of Mechanism Design:
Challenges in the Combination of Interactive Proof Systems, Emilio Jesús Gallego Arias (MINES ParisTech).

I will present joint work with Barthe, Gaboardi, Hsu, Roth, and Strub
[1] on the formal verification of the generic reduction from Bayesian
Incentive Compatible mechanism design to algorithm design given by
Hartline, Kleinberg, and Malekian.

Given agents a₁ ⋯ aₙ, and preferred types t₁ ⋯ tₙ, a mechanism is (a
possibly randomized) function from the inputs (one per agent) to a
single outcome o from a set O, and a real-valued payment pᵢ for each
agent. Agents have a valuation function v(t,o) for each input t and
outcome o.

Informally, we say that that a mechanism is _incentive compatible_ if
every agent can achieve the best utility (valuation minus payment) by
acting according to its preferred type.

The design of effective mechanisms relies on obtaining the true
preferences of agents, incentive compatibility tries to foster agents
to do it.

Formally, a mechanism is Bayesian Incentive Compatible (BIC) if for
every agent i and types tᵢ t'ᵢ, the expected utility is not worse for
the preferred type tᵢ, where expectation is taken over a prior
distribution for the types of other agents.

As mechanisms grow more complex, verification of incentives properties
is important not only for correctness, but also to convince the agents
to act in a truthful way.

To verify the generic reduction, we have used the HOARe2 [2] tool,
which allows to write programs using higher-order relational
refinement types. Relational refinement types can describe properties
pertaining to two different runs of a program, providing a natural way
to express incentive properties, and in particular BIC.

However, HOARe2 is not enough to complete the verification of such a
complex mechanism. The first problem appears as HOARe2 makes extensive
use of the Why3 verification platform, but not every proof obligation
can be automatically discharged by the solvers. We thus prove the
obligations interactively in Coq.

Secondly, HOARe2 is not adequate to prove a crucial "distribution
preserving" property. While HOARe2 works reasonably well to prove
properties that relate two different _runs_ of the same program, this
particular distribution preservation property is proven by showing
an equivalence between different programs.

To that purpose, we have used the program equivalence facilities of
the EasyCrypt theorem prover [3], which allows us to complete the
verification.

[1] "Computer-Aided Verification in Mechanism Design", with Gilles
Barthe, Marco Gaboardi, Justin Hsu, Aaron Roth, and Pierre-Yves
Strub. 12th Conference on Web and Economics (WINE 2016), Montreal,
To Appear.

[2] "Higher-Order Approximate Relational Refinement Types for Mechanism
Design and Differential Privacy", with Gilles Barthe, Marco
Gaboardi, Justin Hsu, Aaron Roth, and Pierre-Yves Strub. POPL 2015.

[3] "Easycrypt: a tutorial" Gilles Barthe and François Dupressoir and
Benjamin Grégoire and César Kunz and Benedikt Schmidt and
Pierre-Yves Strub, Foundations of Security Analysis and Design
VII, LNCS.

**Short Bio:**
Emilio is a postdoctoral researcher at CRI, MINES ParisTech. He works
on formal semantics of Digital Signal Processing and interactive
theorem proving. Previously, he was a postdoctoral appointee in the
privacy group of the University of Pennsylvania working on privacy,
security, software verification, and semantics. He holds a PhD from
the Technical University of Madrid on the categorical and relational
semantics of constraint logic programming.