@inproceedings{e467b747a88d4812a8225e07725447f4,
title = "Computer-aided verification for mechanism design",
abstract = "We explore techniques from computer-aided verification to construct formal proofs of incentive properties. Because formal proofs can be automatically checked, agents do not need to manually check the properties, or even understand the proof. To demonstrate, we present the verification of a sophisticated mechanism: the generic reduction from Bayesian incentive compatible mechanism design to algorithm design given by Hartline, Kleinberg, and Malekian. This mechanism presents new challenges for formal verification, including essential use of randomness from both the execution of the mechanism and from the prior type distributions.",
author = "Gilles Barthe and Marco Gaboardi and Arias, \{Emilio Jes{\'u}s Gallego\} and Justin Hsu and Aaron Roth and Strub, \{Pierre Yves\}",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag GmbH Germany 2016.; 12th International Conference on Web and Internet Economics, WINE 2016 ; Conference date: 11-06-2016 Through 14-07-2016",
year = "2016",
month = jan,
day = "1",
doi = "10.1007/978-3-662-54110-4\_20",
language = "English",
isbn = "9783662541098",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "279--293",
editor = "Adrian Vetta and Yang Cai",
booktitle = "Web and Internet Economics - 12th International Conference, WINE 2016, Proceedings",
}