Projects per year
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.
|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|
|Number of pages||18|
|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||16th ACM Conference on Economics and Computation|
|Period||15/06/15 → 19/06/15|
- formal proof
- mechanized reasoning
- auction theory
FingerprintDive into the research topics of 'Sound auction specification and implementation'. Together they form a unique fingerprint.
- 1 Finished
Kerber, M. & Rowat, C.
1/05/12 → 30/04/15
Project: Research Councils