-
The Exchange Problem
Authors:
Mohit Garg,
Suneel Sarswat
Abstract:
Auctions are widely used in exchanges to match buy and sell requests. Once the buyers and sellers place their requests, the exchange determines how these requests are to be matched. The two most popular objectives used while determining the matching are maximizing volume at a uniform price and maximizing volume with dynamic pricing. In this work, we study the algorithmic complexity of the problems…
▽ More
Auctions are widely used in exchanges to match buy and sell requests. Once the buyers and sellers place their requests, the exchange determines how these requests are to be matched. The two most popular objectives used while determining the matching are maximizing volume at a uniform price and maximizing volume with dynamic pricing. In this work, we study the algorithmic complexity of the problems arising from these matching tasks.
We present a linear time algorithm for uniform price matching which is an improvement over the previous algorithms that take $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-optimal.
△ Less
Submitted 5 March, 2024;
originally announced March 2024.
-
The Design and Regulation of Exchanges: A Formal Approach
Authors:
Mohit Garg,
Suneel Sarswat
Abstract:
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 t…
▽ More
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.
△ Less
Submitted 11 October, 2022;
originally announced October 2022.
-
Verified Double Sided Auctions for Financial Markets
Authors:
Raja Natarajan,
Suneel Sarswat,
Abhishek Kr Singh
Abstract:
Double sided auctions are widely used in financial markets to match demand and supply. Prior works on double sided auctions have focused primarily on single quantity trade requests. We extend various notions of double sided auctions to incorporate multiple quantity trade requests and provide fully formalized matching algorithms for double sided auctions with their correctness proofs. We establish…
▽ More
Double sided auctions are widely used in financial markets to match demand and supply. Prior works on double sided auctions have focused primarily on single quantity trade requests. We extend various notions of double sided auctions to incorporate multiple quantity trade requests and provide fully formalized matching algorithms for double sided auctions with their correctness proofs. We establish new uniqueness theorems that enable automatic detection of violations in an exchange program by comparing its output with that of a verified program. All proofs are formalized in the Coq proof assistant without adding any axiom to the system. We extract verified OCaml and Haskell programs that can be used by the exchanges and the regulators of the financial markets. We demonstrate the practical applicability of our work by running the verified program on real market data from an exchange to automatically check for violations in the exchange algorithm.
△ Less
Submitted 16 April, 2021;
originally announced April 2021.
-
Formally Verified Trades in Financial Markets
Authors:
Suneel Sarswat,
Abhishek Kr Singh
Abstract:
We introduce a formal framework for analyzing trades in financial markets. These days, all big exchanges use computer algorithms to match buy and sell requests and these algorithms must abide by certain regulatory guidelines. For example, market regulators enforce that a matching produced by exchanges should be fair, uniform and individual rational. To verify these properties of trades, we first f…
▽ More
We introduce a formal framework for analyzing trades in financial markets. These days, all big exchanges use computer algorithms to match buy and sell requests and these algorithms must abide by certain regulatory guidelines. For example, market regulators enforce that a matching produced by exchanges should be fair, uniform and individual rational. To verify these properties of trades, we first formally define these notions in a theorem prover and then develop many important results about matching demand and supply. Finally, we use this framework to verify properties of two important classes of double sided auction mechanisms. All the definitions and results presented in this paper are completely formalized in the Coq proof assistant without adding any additional axioms to it.
△ Less
Submitted 18 July, 2020;
originally announced July 2020.
-
Formal verification of trading in financial markets
Authors:
Suneel Sarswat,
Abhishek Kr Singh
Abstract:
We introduce a formal framework for analyzing trades in financial markets. An exchange is where multiple buyers and sellers participate to trade. These days, all big exchanges use computer algorithms that implement double sided auctions to match buy and sell requests and these algorithms must abide by certain regulatory guidelines. For example, market regulators enforce that a matching produced by…
▽ More
We introduce a formal framework for analyzing trades in financial markets. An exchange is where multiple buyers and sellers participate to trade. These days, all big exchanges use computer algorithms that implement double sided auctions to match buy and sell requests and these algorithms must abide by certain regulatory guidelines. For example, market regulators enforce that a matching produced by exchanges should be \emph{fair}, \emph{uniform} and \emph{individual rational}. To verify these properties of trades, we first formally define these notions in a theorem prover and then give formal proofs of relevant results on matchings. Finally, we use this framework to verify properties of two important classes of double sided auctions. All the definitions and results presented in this paper are completely formalised in the Coq proof assistant without adding any additional axioms to it.
△ Less
Submitted 18 July, 2019;
originally announced July 2019.
-
Identifying collusion groups using spectral clustering
Authors:
Suneel Sarswat,
Kandathil Mathew Abraham,
Subir Kumar Ghosh
Abstract:
In an illiquid stock, traders can collude and place orders on a predetermined price and quantity at a fixed schedule. This is usually done to manipulate the price of the stock or to create artificial liquidity in the stock, which may mislead genuine investors. Here, the problem is to identify such group of colluding traders. We modeled the problem instance as a graph, where each trader corresponds…
▽ More
In an illiquid stock, traders can collude and place orders on a predetermined price and quantity at a fixed schedule. This is usually done to manipulate the price of the stock or to create artificial liquidity in the stock, which may mislead genuine investors. Here, the problem is to identify such group of colluding traders. We modeled the problem instance as a graph, where each trader corresponds to a vertex of the graph and trade corresponds to edges of the graph. Further, we assign weights on edges depending on total volume, total number of trades, maximum change in the price and commonality between two vertices. Spectral clustering algorithms are used on the constructed graph to identify colluding group(s). We have compared our results with simulated data to show the effectiveness of spectral clustering to detecting colluding groups. Moreover, we also have used parameters of real data to test the effectiveness of our algorithm.
△ Less
Submitted 17 October, 2016; v1 submitted 22 September, 2015;
originally announced September 2015.
