Sound auction specification and implementation

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Standard

Sound auction specification and implementation. / Caminati, Marco B.; Kerber, Manfred; Lange-Bever, Christoph; Rowat, Colin.

EC '15 Proceedings of the Sixteenth ACM Conference on Economics and Computation . ed. / Tim Roughgarden; Michal Feldman; Michael Schwarz. New York, NY, USA : Association for Computing Machinery , 2015. p. 547-564.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Harvard

Caminati, MB, Kerber, M, Lange-Bever, C & Rowat, C 2015, Sound auction specification and implementation. in T Roughgarden, M Feldman & M Schwarz (eds), EC '15 Proceedings of the Sixteenth ACM Conference on Economics and Computation . Association for Computing Machinery , New York, NY, USA, pp. 547-564, 16th ACM Conference on Economics and Computation, Portland, United States, 15/06/15. https://doi.org/10.1145/2764468.2764511

APA

Caminati, M. B., Kerber, M., Lange-Bever, C., & Rowat, C. (2015). Sound auction specification and implementation. In T. Roughgarden, M. Feldman, & M. Schwarz (Eds.), EC '15 Proceedings of the Sixteenth ACM Conference on Economics and Computation (pp. 547-564). Association for Computing Machinery . https://doi.org/10.1145/2764468.2764511

Vancouver

Caminati MB, Kerber M, Lange-Bever C, Rowat C. Sound auction specification and implementation. In Roughgarden T, Feldman M, Schwarz M, editors, EC '15 Proceedings of the Sixteenth ACM Conference on Economics and Computation . New York, NY, USA: Association for Computing Machinery . 2015. p. 547-564 https://doi.org/10.1145/2764468.2764511

Author

Caminati, Marco B. ; Kerber, Manfred ; Lange-Bever, Christoph ; Rowat, Colin. / Sound auction specification and implementation. EC '15 Proceedings of the Sixteenth ACM Conference on Economics and Computation . editor / Tim Roughgarden ; Michal Feldman ; Michael Schwarz. New York, NY, USA : Association for Computing Machinery , 2015. pp. 547-564

Bibtex

@inproceedings{98224376b5964c609b422523853e05a4,
title = "Sound auction specification and implementation",
abstract = "We introduce `formal methods' of mechanized reasoning from computer science to address two problems in auction design and practice: is a given auction design soundly specified, possessing its intended properties; and, is the design faithfully implemented when actually run? Failure on either front can be hugely costly in large auctions. In the familiar setting of the combinatorial Vickrey auction, we use a mechanized reasoner, Isabelle, to first ensure that the auction has a set of desired properties (e.g. allocating all items at non-negative prices), and to then generate verified executable code directly from the specified design. Having established the expected results in a known context, we intend next to use formal methods to verify new auction designs.",
keywords = "formal proof, mechanized reasoning, auction theory",
author = "Caminati, {Marco B.} and Manfred Kerber and Christoph Lange-Bever and Colin Rowat",
year = "2015",
month = jun
day = "15",
doi = "10.1145/2764468.2764511",
language = "English",
pages = "547--564",
editor = "Roughgarden, {Tim } and Michal Feldman and Michael Schwarz",
booktitle = "EC '15 Proceedings of the Sixteenth ACM Conference on Economics and Computation",
publisher = "Association for Computing Machinery ",
note = "16th ACM Conference on Economics and Computation ; Conference date: 15-06-2015 Through 19-06-2015",

}

RIS

TY - GEN

T1 - Sound auction specification and implementation

AU - Caminati, Marco B.

AU - Kerber, Manfred

AU - Lange-Bever, Christoph

AU - Rowat, Colin

PY - 2015/6/15

Y1 - 2015/6/15

N2 - We introduce `formal methods' of mechanized reasoning from computer science to address two problems in auction design and practice: is a given auction design soundly specified, possessing its intended properties; and, is the design faithfully implemented when actually run? Failure on either front can be hugely costly in large auctions. In the familiar setting of the combinatorial Vickrey auction, we use a mechanized reasoner, Isabelle, to first ensure that the auction has a set of desired properties (e.g. allocating all items at non-negative prices), and to then generate verified executable code directly from the specified design. Having established the expected results in a known context, we intend next to use formal methods to verify new auction designs.

AB - We introduce `formal methods' of mechanized reasoning from computer science to address two problems in auction design and practice: is a given auction design soundly specified, possessing its intended properties; and, is the design faithfully implemented when actually run? Failure on either front can be hugely costly in large auctions. In the familiar setting of the combinatorial Vickrey auction, we use a mechanized reasoner, Isabelle, to first ensure that the auction has a set of desired properties (e.g. allocating all items at non-negative prices), and to then generate verified executable code directly from the specified design. Having established the expected results in a known context, we intend next to use formal methods to verify new auction designs.

KW - formal proof

KW - mechanized reasoning

KW - auction theory

U2 - 10.1145/2764468.2764511

DO - 10.1145/2764468.2764511

M3 - Conference contribution

SP - 547

EP - 564

BT - EC '15 Proceedings of the Sixteenth ACM Conference on Economics and Computation

A2 - Roughgarden, Tim

A2 - Feldman, Michal

A2 - Schwarz, Michael

PB - Association for Computing Machinery

CY - New York, NY, USA

T2 - 16th ACM Conference on Economics and Computation

Y2 - 15 June 2015 through 19 June 2015

ER -