A proof-carrying code approach to certificate auction mechanisms

W. Bai*, E. M. Tadjouddine, T. R. Payne, S. U. Guan

*Corresponding author for this work

Research output: Chapter in Book or Report/Conference proceedingConference Proceedingpeer-review

2 Citations (Scopus)


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.

Original languageEnglish
Title of host publicationFormal Aspects of Component Software - 10th International Symposium, FACS 2013, Revised Selected Papers
PublisherSpringer Verlag
Number of pages18
ISBN (Print)9783319076010
Publication statusPublished - 2014
Event10th International Symposium on Formal Aspects of Component Software, FACS 2013 - Nanchang, China
Duration: 27 Oct 201329 Oct 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8348 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference10th International Symposium on Formal Aspects of Component Software, FACS 2013


  • Certification
  • Coq
  • E-commerce
  • Proof-carrying code
  • Software agents

Cite this