Sound auction specification and implementation

Marco B. Caminati; Manfred Kerber; Christoph Lange-Bever; Colin Rowat

doi:10.1145/2764468.2764511

Sound auction specification and implementation

Marco B. Caminati, Manfred Kerber, Christoph Lange-Bever, Colin Rowat

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

8 Citations (Scopus)

221 Downloads (Pure)

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.

Original language	English
Title of host publication	EC '15 Proceedings of the Sixteenth ACM Conference on Economics and Computation
Editors	Tim Roughgarden, Michal Feldman, Michael Schwarz
Place of Publication	New York, NY, USA
Publisher	Association for Computing Machinery
Pages	547-564
Number of pages	18
ISBN (Electronic)	978-1-4503-3410-5
DOIs	https://doi.org/10.1145/2764468.2764511
Publication status	Published - 15 Jun 2015
Event	16th ACM Conference on Economics and Computation - http://www.sigecom.org/ec15/, Portland, United States Duration: 15 Jun 2015 → 19 Jun 2015

Conference

Conference	16th ACM Conference on Economics and Computation
Country/Territory	United States
City	Portland
Period	15/06/15 → 19/06/15

Keywords

formal proof
mechanized reasoning
auction theory

Access to Document

10.1145/2764468.2764511

Caminati_et_al_2015_Sound_auction_specification_ACM_EC15_Proceedings
Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage, and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the owner/author(s). Copyright is held by the author/owner(s). Eligibility for repository : checked 18/12/2015
Final published version, 941 KBLicence: Other (please specify with Rights Statement)

http://dl.acm.org/citation.cfm?doid=2764468.2764511

Formal Representation and Proof for Cooperative Games: A Foundation for Complex Social Behaviour
Kerber, M. & Rowat, C.
Engineering & Physical Science Research Council
1/05/12 → 30/04/15
Project: Research Councils

Cite this

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

}

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

Sound auction specification and implementation. / Caminati, Marco B.; Kerber, Manfred; Lange-Bever, Christoph et al.
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 proceeding › Conference contribution

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 -

Sound auction specification and implementation

Abstract

Conference

Keywords

Access to Document

Fingerprint

Projects

Formal Representation and Proof for Cooperative Games: A Foundation for Complex Social Behaviour

Cite this