Caminati, Marco B.Marco B.CaminatiKerber, ManfredManfredKerberLange, ChristophChristophLangeRowat, C.C.Rowat2022-03-132022-03-132015https://publica.fraunhofer.de/handle/publica/39507510.1145/2764468.2764511We 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.en005conference paper