Reasoning about Dynamic Auctions

Research output: Contribution to conference (unpublished)Abstract

Colleges, School and Institutes

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.

Details

Original languageEnglish
Pages15-16
Number of pages2
Publication statusPublished - 9 Apr 2015
EventAutomated Reasoning Workshop (ARW) - http://events.cs.bham.ac.uk/arw15/, Birmingham, United Kingdom
Duration: 9 Apr 201510 Apr 2015

Conference

ConferenceAutomated Reasoning Workshop (ARW)
CountryUnited Kingdom
CityBirmingham
Period9/04/1510/04/15