Reasoning about Dynamic Auctions

Marco B. Caminati, Manfred Kerber, Colin Rowat

Research output: Contribution to conference (unpublished)Abstract


Auctions are used to sell goods worth trillions of dollars annually.
Many of them are well established, frequently used, and hence well tested.
However, in some domains new auction schemes are developed and only infrequently used. These can benefit most from formal methods.
We report here how verified code can be extracted using Isabelle's extraction mechanism for so-called dynamic auctions, that is, auctions in which participants can bid in several rounds.
We use co-recursion in order to reason about and extract code for dynamic auctions in which inputs and computations are interleaved.
Original languageEnglish
Number of pages2
Publication statusPublished - 9 Apr 2015
EventAutomated Reasoning Workshop (ARW) -, Birmingham, United Kingdom
Duration: 9 Apr 201510 Apr 2015


ConferenceAutomated Reasoning Workshop (ARW)
Country/TerritoryUnited Kingdom


Dive into the research topics of 'Reasoning about Dynamic Auctions'. Together they form a unique fingerprint.

Cite this