Sound auction specification and implementation
- Submitting institution
-
University of St Andrews
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 267801129
- Type
- E - Conference contribution
- DOI
-
10.1145/2764468.2764511
- Title of conference / published proceedings
- Proceedings of the Sixteenth ACM Conference on Economics and Computation (EC '15)
- First page
- 547
- Volume
- -
- Issue
- -
- ISSN
- -
- Open access status
- -
- Month of publication
- June
- Year of publication
- 2015
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
3
- Research group(s)
-
C - Health Informatics
- Citation count
- -
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Formal methods underpin the most rigorous assurance standards, such as EAL levels 5-7.
Their deployment to software handling high risk or cost applications is arguably worth the cost, given notable, disastrous failures happened in high stakes industries such as trading and aero-space.
This pioneering paper shows that theorem proving is indeed applicable to the domain of combinatorial auctions, concretely adopted, for example, in spectrum auctions moving millions of pounds, and featuring amounts of combinations intractable by other formal methods such as model checking.
Executable definitions are proven correct (e.g., they terminate and maximize bids value) by machine verified theorems.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -
