Hier finden Sie wissenschaftliche Publikationen aus den Fraunhofer-Instituten.

Sound auction specification and implementation

: Caminati, M.B.; Kerber, M.; Lange, C.; Rowat, C.


Association for Computing Machinery -ACM-:
16th ACM Conference on Economics and Computation, EC 2015. Proceedings : Portland, Oregon, USA, June 15 - 19, 2015
New York: ACM, 2015
ISBN: 978-1-4503-3410-5
Conference on Economics and Computation (EC) <16, 2015, Portland/Or.>
Fraunhofer IAIS ()

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 nonnegative 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.