Sound auction specification and implementation

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

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

8 Citations (Scopus)
170 Downloads (Pure)


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
Place of PublicationNew York, NY, USA
PublisherAssociation for Computing Machinery
Number of pages18
ISBN (Electronic)978-1-4503-3410-5
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
Country/TerritoryUnited States


  • formal proof
  • mechanized reasoning
  • auction theory


Dive into the research topics of 'Sound auction specification and implementation'. Together they form a unique fingerprint.

Cite this