Sound Auction Specification and Implementation

Marco B Caminati, Manfred Kerber, Christoph Lange and Colin Rowat

Discussion Papers from Department of Economics, University of Birmingham

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 (search for similar items in EconPapers)
JEL-codes: B41 C63 C88 D44 (search for similar items in EconPapers)
Pages: We intro
Date: 2015-03
References: View references in EconPapers View complete reference list from CitEc
Citations: View citations in EconPapers (3)

Downloads: (external link)
https://repec.cal.bham.ac.uk/pdf/15-08.pdf

Related works:
This item may be available elsewhere in EconPapers: Search for items with the same title.

Export reference: BibTeX RIS (EndNote, ProCite, RefMan) HTML/Text

Persistent link: https://EconPapers.repec.org/RePEc:bir:birmec:15-08

Access Statistics for this paper

More papers in Discussion Papers from Department of Economics, University of Birmingham Contact information at EDIRC.
Bibliographic data for series maintained by Oleksandr Talavera ().