论文标题
交流的设计和调节：一种形式的方法
The Design and Regulation of Exchanges: A Formal Approach
论文作者
论文摘要
我们使用正式的方法来指定，设计和监视连续的双重拍卖，这些拍卖被广泛用于匹配外币，股票和商品交换的买卖双方。我们确定了此类拍卖的三个自然特性，并正式证明这些特性完全确定了输入输出关系。然后，我们正式验证天然算法是否满足这些特性。所有定义，定理和证明都是在交互式定理供体中形式化的。我们提取算法的验证程序，以构建一个自动检查器，如果它们产生违反任何自然属性的交易，则可以保证在交易所的交易日志中检测错误。
We use formal methods to specify, design, and monitor continuous double auctions, which are widely used to match buyers and sellers at exchanges of foreign currencies, stocks, and commodities. We identify three natural properties of such auctions and formally prove that these properties completely determine the input-output relationship. We then formally verify that a natural algorithm satisfies these properties. All definitions, theorems, and proofs are formalized in an interactive theorem prover. We extract a verified program of our algorithm to build an automated checker that is guaranteed to detect errors in the trade logs of exchanges if they generate transactions that violate any of the natural properties.
