Sound auction specification and implementation

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

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

8 Citations (Scopus)


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 publicationProceedings of the Sixteenth ACM Conference on Economics and Computation (EC '15)
Place of PublicationNew York
ISBN (Print)9781450334105
Publication statusPublished - 15 Jun 2015


  • 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