Computer-aided verification for mechanism design

Gilles Barthe; Marco Gaboardi; Emilio Jesús Gallego Arias; Justin Hsu; Aaron Roth; Pierre Yves Strub

doi:10.1007/978-3-662-54110-4_20

Computer-aided verification for mechanism design

Gilles Barthe
, Marco Gaboardi
, Emilio Jesús Gallego Arias
, Justin Hsu
, Aaron Roth
, Pierre Yves Strub

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	Web and Internet Economics - 12th International Conference, WINE 2016, Proceedings
Editors	Adrian Vetta, Yang Cai
Publisher	Springer Verlag
Pages	279-293
Number of pages	15
ISBN (Print)	9783662541098
DOIs	https://doi.org/10.1007/978-3-662-54110-4_20
Publication status	Published - 1 Jan 2016
Externally published	Yes
Event	12th International Conference on Web and Internet Economics, WINE 2016 - Montreal, Canada Duration: 11 Jun 2016 → 14 Jul 2016

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10123 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	12th International Conference on Web and Internet Economics, WINE 2016
Country/Territory	Canada
City	Montreal
Period	11/06/16 → 14/07/16

Access to Document

10.1007/978-3-662-54110-4_20

Cite this

Barthe, G., Gaboardi, M., Arias, E. J. G., Hsu, J., Roth, A., & Strub, P. Y. (2016). Computer-aided verification for mechanism design. In A. Vetta, & Y. Cai (Eds.), Web and Internet Economics - 12th International Conference, WINE 2016, Proceedings (pp. 279-293). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10123 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-662-54110-4_20

Barthe, Gilles ; Gaboardi, Marco ; Arias, Emilio Jesús Gallego et al. / Computer-aided verification for mechanism design. Web and Internet Economics - 12th International Conference, WINE 2016, Proceedings. editor / Adrian Vetta ; Yang Cai. Springer Verlag, 2016. pp. 279-293 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@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",

}

Barthe, G, Gaboardi, M, Arias, EJG, Hsu, J, Roth, A & Strub, PY 2016, Computer-aided verification for mechanism design. in A Vetta & Y Cai (eds), Web and Internet Economics - 12th International Conference, WINE 2016, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10123 LNCS, Springer Verlag, pp. 279-293, 12th International Conference on Web and Internet Economics, WINE 2016, Montreal, Canada, 11/06/16. https://doi.org/10.1007/978-3-662-54110-4_20

Computer-aided verification for mechanism design. / Barthe, Gilles; Gaboardi, Marco; Arias, Emilio Jesús Gallego et al.
Web and Internet Economics - 12th International Conference, WINE 2016, Proceedings. ed. / Adrian Vetta; Yang Cai. Springer Verlag, 2016. p. 279-293 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10123 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Computer-aided verification for mechanism design

AU - Barthe, Gilles

AU - Gaboardi, Marco

AU - Arias, Emilio Jesús Gallego

AU - Hsu, Justin

AU - Roth, Aaron

AU - Strub, Pierre Yves

N1 - Publisher Copyright: © Springer-Verlag GmbH Germany 2016.

PY - 2016/1/1

Y1 - 2016/1/1

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/85007407018

U2 - 10.1007/978-3-662-54110-4_20

DO - 10.1007/978-3-662-54110-4_20

M3 - Conference contribution

AN - SCOPUS:85007407018

SN - 9783662541098

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 279

EP - 293

BT - Web and Internet Economics - 12th International Conference, WINE 2016, Proceedings

A2 - Vetta, Adrian

A2 - Cai, Yang

PB - Springer Verlag

T2 - 12th International Conference on Web and Internet Economics, WINE 2016

Y2 - 11 June 2016 through 14 July 2016

ER -

Barthe G, Gaboardi M, Arias EJG, Hsu J, Roth A, Strub PY. Computer-aided verification for mechanism design. In Vetta A, Cai Y, editors, Web and Internet Economics - 12th International Conference, WINE 2016, Proceedings. Springer Verlag. 2016. p. 279-293. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-662-54110-4_20

Computer-aided verification for mechanism design

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this