Exchanges such as that of foreign currency, stocks, and commodities are organized marketplaces where trades are conducted by matching buy and sell requests of traders. Several instances have been reported where exchanges have been found violating regulatory guidelines and the stated rules. In this work, we propose a robust approach to exchange design and regulation by presenting a comprehensive framework for formalizing and certifying double auctions, which are the key mechanisms employed by the exchanges to match the buy and sell requests of traders. Typically, two types of double auctions are employed in the exchanges: call auctions and continuous auctions. For call auctions again, there are two main alternatives: uniform price and dynamic price. Our main contributions are as follows.
-- Call auctions: We formalize the various notions of call auctions and provide fully formalized algorithms for uniform and dynamic price auctions along with their correctness proofs.
-- Continuous auctions: We formulate the specifications for continuous double auctions by identifying three simple and necessary properties and formally proving that they are in fact sufficient; they completely determine the input-output relationship. We then formally verify that a natural algorithm satisfies these properties.
-- Uniqueness theorems: We establish new uniqueness theorems for both call and continuous auctions that enable us to build automated checkers that are guaranteed to detect errors in the trade logs of exchanges if they generate transactions that violate the specifications. We extract verified programs of our formalized algorithms to build automated checkers.
-- Tests on real data: We add preprocessing steps that enable us to tailor our general model to a specific exchange. We then run our automated checkers on real data. Furthermore, we report the running times on various input sizes.
-- Efficiency: We obtain tight bounds on the time complexity of all these three matching problems in the comparison model. Specifically, we demonstrate that uniform price matching can be achieved in linear time, which is an improvement over the previous algorithm that takes O(n log n) time to match n requests. For dynamic price matching, we establish a lower bound of Ω(n log n) on the running time, thereby proving that the currently known best algorithm is time-efficient. Furthermore, for continuous double auctions, we show that a natural algorithm takes O(n log n) time, while any algorithm requires at least Ω(n log n) time.
