IDEAS home Printed from https://ideas.repec.org/p/arx/papers/2210.05447.html
   My bibliography  Save this paper

The Design and Regulation of Exchanges: A Formal Approach

Author

Listed:
  • 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 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.

Suggested Citation

  • Mohit Garg & Suneel Sarswat, 2022. "The Design and Regulation of Exchanges: A Formal Approach," Papers 2210.05447, arXiv.org.
    • Handle: RePEc:arx:papers:2210.05447
    as

    Download full text from publisher

    File URL: http://arxiv.org/pdf/2210.05447
    File Function: Latest version
    Download Restriction: no
    ---><---

    References listed on IDEAS

    as
    1. Vasilios Mavroudis & Hayden Melton, 2019. "Libra: Fair Order-Matching for Electronic Financial Exchanges," Papers 1910.00321, arXiv.org.
    2. van Lith, Bart S. & ten Thije Boonkkamp, Jan H.M. & IJzerman, Wilbert L., 2018. "Full linear multistep methods as root-finders," Applied Mathematics and Computation, Elsevier, vol. 320(C), pages 190-201.
    3. Zhu, Qianqian & Zheng, Yao & Li, Guodong, 2018. "Linear double autoregression," Journal of Econometrics, Elsevier, vol. 207(1), pages 162-174.
    4. Jinzhong Niu & Simon Parsons, 2013. "Maximizing Matching in Double-sided Auctions," Papers 1304.3135, arXiv.org.
    5. Yingbo Li & Merlise A. Clyde, 2018. "Mixtures of g-Priors in Generalized Linear Models," Journal of the American Statistical Association, Taylor & Francis Journals, vol. 113(524), pages 1828-1845, October.
    Full references (including those not matched with items on IDEAS)

    Most related items

    These are the items that most often cite the same works as this one and are cited by the same works as this one.
    1. Kai Yang & Qingqing Zhang & Xinyang Yu & Xiaogang Dong, 2023. "Bayesian inference for a mixture double autoregressive model," Statistica Neerlandica, Netherlands Society for Statistics and Operations Research, vol. 77(2), pages 188-207, May.
    2. Suneel Sarswat & Abhishek Kr Singh, 2020. "Formally Verified Trades in Financial Markets," Papers 2007.10805, arXiv.org.
    3. Mark F. J. Steel, 2020. "Model Averaging and Its Use in Economics," Journal of Economic Literature, American Economic Association, vol. 58(3), pages 644-719, September.
    4. Miyashita, Kazuo, 2015. "Developing an Online Market Mechanism for Trading Perishable Agricultural Commodities," 2015 Conference, August 9-14, 2015, Milan, Italy 212470, International Association of Agricultural Economists.
    5. Guo, Shaojun & Li, Dong & Li, Muyi, 2019. "Strict stationarity testing and GLAD estimation of double autoregressive models," Journal of Econometrics, Elsevier, vol. 211(2), pages 319-337.
    6. Abdullah M. Alabdullatif & Enrico H. Gerding & Alvaro Perez-Diaz, 2020. "Market Design and Trading Strategies for Community Energy Markets with Storage and Renewable Supply," Energies, MDPI, vol. 13(4), pages 1-31, February.
    7. Songhua Tan & Qianqian Zhu, 2022. "Asymmetric linear double autoregression," Journal of Time Series Analysis, Wiley Blackwell, vol. 43(3), pages 371-388, May.
    8. Guo, Shaojun & Li, Dong & Li, Muyi, 2018. "Strict Stationarity Testing and GLAD Estimation of Double Autoregressive Models," IRTG 1792 Discussion Papers 2018-049, Humboldt University of Berlin, International Research Training Group 1792 "High Dimensional Nonstationary Time Series".
    9. Suneel Sarswat & Abhishek Kr Singh, 2019. "Formal verification of trading in financial markets," Papers 1907.07885, arXiv.org.
    10. Kirsner, Daniel & Sansó, Bruno, 2020. "Multi-scale shotgun stochastic search for large spatial datasets," Computational Statistics & Data Analysis, Elsevier, vol. 146(C).
    11. Vasilios Mavroudis, 2019. "Bounded Temporal Fairness for FIFO Financial Markets," Papers 1911.09209, arXiv.org.
    12. Huan Gong & Dong Li, 2020. "On the three‐step non‐Gaussian quasi‐maximum likelihood estimation of heavy‐tailed double autoregressive models," Journal of Time Series Analysis, Wiley Blackwell, vol. 41(6), pages 883-891, November.
    13. Arnab Kumar Maity & Sanjib Basu & Santu Ghosh, 2021. "Bayesian criterion‐based variable selection," Journal of the Royal Statistical Society Series C, Royal Statistical Society, vol. 70(4), pages 835-857, August.
    14. Zhang, Wenjie & Quan, Hao & Srinivasan, Dipti, 2018. "Parallel and reliable probabilistic load forecasting via quantile regression forest and quantile determination," Energy, Elsevier, vol. 160(C), pages 810-819.
    15. Ho, Manh-Toan & La, Viet-Phuong & Nguyen, Minh-Hoang & Pham, Thanh-Hang & Vuong, Thu-Trang & Vuong, Ha-My & Pham, Hung-Hiep & Hoang, Anh-Duc & Vuong, Quan-Hoang, 2020. "An analytical view on STEM education and outcomes: Examples of the social gap and gender disparity in Vietnam," Children and Youth Services Review, Elsevier, vol. 119(C).
    16. Haeringer, Guillaume & Melton, Hayden, 2020. "High Frequency Fairness," MPRA Paper 103907, University Library of Munich, Germany.
    17. Hans, Christopher M. & Peruggia, Mario & Wang, Junyan, 2023. "Empirical Bayes Model Averaging with Influential Observations: Tuning Zellner’s g Prior for Predictive Robustness," Econometrics and Statistics, Elsevier, vol. 27(C), pages 102-119.
    18. Yu-Fang Chien & Haiming Zhou & Timothy Hanson & Theodore Lystig, 2023. "Informative g -Priors for Mixed Models," Stats, MDPI, vol. 6(1), pages 1-23, January.
    19. Saralees Nadarajah & Malick Kebe, 2023. "The Confluent Hypergeometric Beta Distribution," Mathematics, MDPI, vol. 11(9), pages 1-23, May.
    20. Li, Dong & Tao, Yuxin & Yang, Yaxing & Zhang, Rongmao, 2023. "Maximum likelihood estimation for α-stable double autoregressive models," Journal of Econometrics, Elsevier, vol. 236(1).

    More about this item

    NEP fields

    This paper has been announced in the following NEP Reports:

    Statistics

    Access and download statistics

    Corrections

    All material on this site has been provided by the respective publishers and authors. You can help correct errors and omissions. When requesting a correction, please mention this item's handle: RePEc:arx:papers:2210.05447. See general information about how to correct material in RePEc.

    If you have authored this item and are not yet registered with RePEc, we encourage you to do it here. This allows to link your profile to this item. It also allows you to accept potential citations to this item that we are uncertain about.

    If CitEc recognized a bibliographic reference but did not link an item in RePEc to it, you can help with this form .

    If you know of missing items citing this one, you can help us creating those links by adding the relevant references in the same way as above, for each refering item. If you are a registered author of this item, you may also want to check the "citations" tab in your RePEc Author Service profile, as there may be some citations waiting for confirmation.

    For technical questions regarding this item, or to correct its authors, title, abstract, bibliographic or download information, contact: arXiv administrators (email available below). General contact details of provider: http://arxiv.org/ .

    Please note that corrections may take a couple of weeks to filter through the various RePEc services.

    IDEAS is a RePEc service. RePEc uses bibliographic data supplied by the respective publishers.