Home > Research > Publications & Outputs > Sound auction specification and implementation

Research

Associated organisational unit

Text available via DOI:

View graph of relations

Sound auction specification and implementation

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review

Published

Standard

Sound auction specification and implementation. / Caminati, Marco B.; Kerber, Manfred; Lange, Christoph et al.
Proceedings of the Sixteenth ACM Conference on Economics and Computation (EC '15). ACM, 2015. p. 547-564.

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review

Harvard

Caminati, MB, Kerber, M, Lange, C & Rowat, C 2015, Sound auction specification and implementation. in Proceedings of the Sixteenth ACM Conference on Economics and Computation (EC '15). ACM, pp. 547-564. https://doi.org/10.1145/2764468.2764511

APA

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

Vancouver

Caminati MB, Kerber M, Lange C, Rowat C. Sound auction specification and implementation. In Proceedings of the Sixteenth ACM Conference on Economics and Computation (EC '15). ACM. 2015. p. 547-564 doi: 10.1145/2764468.2764511

Author

Caminati, Marco B. ; Kerber, Manfred ; Lange, Christoph et al. / Sound auction specification and implementation. Proceedings of the Sixteenth ACM Conference on Economics and Computation (EC '15). ACM, 2015. pp. 547-564

Bibtex

@inproceedings{54dd975e7a92402ca8e6f4e83d7b20a4,
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.",
author = "Caminati, {Marco B.} and Manfred Kerber and Christoph Lange and Colin Rowat",
year = "2015",
month = jun,
day = "15",
doi = "10.1145/2764468.2764511",
language = "English",
isbn = "9781450334105",
pages = "547--564",
booktitle = "Proceedings of the Sixteenth ACM Conference on Economics and Computation (EC '15)",
publisher = "ACM",

}

RIS

TY - GEN

T1 - Sound auction specification and implementation

AU - Caminati, Marco B.

AU - Kerber, Manfred

AU - Lange, 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.

U2 - 10.1145/2764468.2764511

DO - 10.1145/2764468.2764511

M3 - Conference contribution/Paper

SN - 9781450334105

SP - 547

EP - 564

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

PB - ACM

ER -