@inproceedings{7c9cf1e0f13c4d77896db582f72445f8,
title = "A proof-carrying code approach to certificate auction mechanisms",
abstract = "Whilst it can be highly desirable for software agents to engage in auctions, they are normally restricted to trading within known auctions, due to the complexity and heterogeneity of the auction rules within an e-commerce system. To allow for agents to deal with previously unseen protocols, we present a proof-carrying code approach using Coq wherein auction protocols can be specified and desirable properties be proven. This enables software agents to automatically certify claimed auction properties and assist them in their decision-making. We have illustrated our approach by specifying both the English and Vickrey auctions; have formalized different bidding strategies for agents; have certified that up to the valuation is the optimal strategy in English auction and truthful bidding is the optimal strategy in Vickrey auction for all agents. The formalization and certification are based on inductive definitions and constructions from within Coq. This work contributes to solving the problem of open societies of software agents moving between different institutions and seeking to make optimal decisions and will benefit those engaged in agent-mediated e-commerce.",
keywords = "Certification, Coq, E-commerce, Proof-carrying code, Software agents",
author = "W. Bai and Tadjouddine, {E. M.} and Payne, {T. R.} and Guan, {S. U.}",
year = "2014",
doi = "10.1007/978-3-319-07602-7_4",
language = "English",
isbn = "9783319076010",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "23--40",
booktitle = "Formal Aspects of Component Software - 10th International Symposium, FACS 2013, Revised Selected Papers",
note = "10th International Symposium on Formal Aspects of Component Software, FACS 2013 ; Conference date: 27-10-2013 Through 29-10-2013",
}