声音拍卖规范和实现-研究论文

我们从计算机科学中引入了机械化推理的“形式方法”，以解决拍卖设计和实践中的两个问题：给定的拍卖设计是否经过合理指定，具有其预期属性； 以及，实际运行时是否忠实地实现了设计？ 在大型拍卖中，任一方面的失败都会造成巨大的代价。 在熟悉的组合 Vickrey 拍卖设置中，我们使用机械化推理器 Isabelle，首先确保拍卖具有一组所需的属性（例如，以非负价格分配所有物品），然后直接生成经过验证的可执行代码从指定的设计。 在已知背景下确定预期结果后，我们接下来打算使用正式方法来验证新的拍卖设计。