Sound auction specification and implementation

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

Colleges, School and Institutes


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 languageEnglish
Title of host publicationEC '15 Proceedings of the Sixteenth ACM Conference on Economics and Computation
EditorsTim Roughgarden, Michal Feldman, Michael Schwarz
Publication statusPublished - 15 Jun 2015
Event16th ACM Conference on Economics and Computation -, Portland, United States
Duration: 15 Jun 201519 Jun 2015


Conference16th ACM Conference on Economics and Computation
CountryUnited States


  • formal proof, mechanized reasoning, auction theory