Home > Research > Publications & Outputs > Proving soundness of combinatorial Vickrey auct...

Research

Associated organisational unit

Text available via DOI:

View graph of relations

Proving soundness of combinatorial Vickrey auctions and generating verified executable code

Research output: Working paper › Preprint

Published

Standard

Proving soundness of combinatorial Vickrey auctions and generating verified executable code. / Caminati, Marco B; Kerber, Manfred; Lange, Christoph et al.
2013. (arXiv preprint arXiv:1308.1779).

Research output: Working paper › Preprint

Harvard

Caminati, MB, Kerber, M, Lange, C & Rowat, C 2013 'Proving soundness of combinatorial Vickrey auctions and generating verified executable code' arXiv preprint arXiv:1308.1779. https://doi.org/10.48550/arXiv.1308.1779

APA

Caminati, M. B., Kerber, M., Lange, C., & Rowat, C. (2013). Proving soundness of combinatorial Vickrey auctions and generating verified executable code. (arXiv preprint arXiv:1308.1779). https://doi.org/10.48550/arXiv.1308.1779

Vancouver

Caminati MB, Kerber M, Lange C, Rowat C. Proving soundness of combinatorial Vickrey auctions and generating verified executable code. 2013 Aug 8. (arXiv preprint arXiv:1308.1779). doi: 10.48550/arXiv.1308.1779

Author

Caminati, Marco B ; Kerber, Manfred ; Lange, Christoph et al. / Proving soundness of combinatorial Vickrey auctions and generating verified executable code. 2013. (arXiv preprint arXiv:1308.1779).

Bibtex

@techreport{09a729b2b28c4edfb8f3d8883055eb32,
title = "Proving soundness of combinatorial Vickrey auctions and generating verified executable code",
abstract = "Using mechanised reasoning we prove that combinatorial Vickrey auctions are soundly specified in that they associate a unique outcome (allocation and transfers) to any valid input (bids). Having done so, we auto-generate verified executable code from the formally defined auction. This removes a source of error in implementing the auction design. We intend to use formal methods to verify new auction designs. Here, our contribution is to introduce and demonstrate the use of formal methods for auction verification in the familiar setting of a well-known auction.",
author = "Caminati, {Marco B} and Manfred Kerber and Christoph Lange and Colin Rowat",
year = "2013",
month = aug,
day = "8",
doi = "10.48550/arXiv.1308.1779",
language = "English",
series = "arXiv preprint arXiv:1308.1779",
type = "WorkingPaper",

}

RIS

TY - UNPB

T1 - Proving soundness of combinatorial Vickrey auctions and generating verified executable code

AU - Caminati, Marco B

AU - Kerber, Manfred

AU - Lange, Christoph

AU - Rowat, Colin

PY - 2013/8/8

Y1 - 2013/8/8

N2 - Using mechanised reasoning we prove that combinatorial Vickrey auctions are soundly specified in that they associate a unique outcome (allocation and transfers) to any valid input (bids). Having done so, we auto-generate verified executable code from the formally defined auction. This removes a source of error in implementing the auction design. We intend to use formal methods to verify new auction designs. Here, our contribution is to introduce and demonstrate the use of formal methods for auction verification in the familiar setting of a well-known auction.

AB - Using mechanised reasoning we prove that combinatorial Vickrey auctions are soundly specified in that they associate a unique outcome (allocation and transfers) to any valid input (bids). Having done so, we auto-generate verified executable code from the formally defined auction. This removes a source of error in implementing the auction design. We intend to use formal methods to verify new auction designs. Here, our contribution is to introduce and demonstrate the use of formal methods for auction verification in the familiar setting of a well-known auction.

U2 - 10.48550/arXiv.1308.1779

DO - 10.48550/arXiv.1308.1779

M3 - Preprint

T3 - arXiv preprint arXiv:1308.1779

BT - Proving soundness of combinatorial Vickrey auctions and generating verified executable code

ER -