Document Open Access Logo

The Design and Regulation of Exchanges: A Formal Approach

Authors Mohit Garg, Suneel Sarswat

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2022.39.pdf
  • Filesize: 1.06 MB
  • 21 pages

Document Identifiers

Author Details

Mohit Garg
  • University of Bremen, Bremen, Germany
  • University of Hamburg, Hamburg, Germany
Suneel Sarswat
  • Tata Institute of Fundamental Research, Mumbai, India

Cite As Get BibTex

Mohit Garg and Suneel Sarswat. The Design and Regulation of Exchanges: A Formal Approach. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 39:1-39:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.FSTTCS.2022.39

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.

Subject Classification

ACM Subject Classification
  • Applied computing → Online auctions
  • Software and its engineering → Software verification and validation
  • Software and its engineering → Correctness
Keywords
  • Double Auctions
  • Formal Specification and Verification
  • Financial Markets

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Supplementary materials: Coq formalization and demonstration, 2022. URL: https://github.com/suneel-sarswat/cda.
  2. Iliano Cervesato, Sharjeel Khan, Giselle Reis, and Dragisa Žunić. Formalization of automated trading systems in a concurrent linear framework. In Linearity-TLLA@FLoC, volume 292 of EPTCS, pages 1-14, 2018. URL: http://arxiv.org/abs/1904.06159.
  3. Frankfurt Stock Exchange. Market Model for the Trading Venue Xetra. https://www.xetra.com/resource/blob/1963528/ceda0de49d5b8db5e33cdb17375e4cc9/data/T7_R.8.1_Market_Model-en.pdf, Sep 22, 2021.
  4. Daniel Friedman. The double auction market institution: A survey. The double auction market: Institutions, theories, and evidence, 14:3-25, 1993. Google Scholar
  5. Larry Harris. Trading and exchanges: Market microstructure for practitioners. OUP USA, 2003. Google Scholar
  6. Cezary Kaliszyk and Julian Parsert. Formal microeconomic foundations and the first welfare theorem. In June Andronick and Amy P. Felty, editors, Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, January 8-9, 2018, pages 91-101. ACM, 2018. URL: https://doi.org/10.1145/3167100.
  7. Vasilios Mavroudis and Hayden Melton. Libra: Fair order-matching for electronic financial exchanges. In Proceedings of the 1st ACM Conference on Advances in Financial Technologies, pages 156-168, 2019. Google Scholar
  8. Raja Natarajan, Suneel Sarswat, and Abhishek Kr Singh. Verified double sided auctions for financial markets. In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29 to July 1, 2021, Rome, Italy (Virtual Conference), volume 193 of LIPIcs, pages 28:1-28:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.ITP.2021.28.
  9. Jinzhong Niu and Simon Parsons. Maximizing matching in double-sided auctions. In International conference on Autonomous Agents and Multi-Agent Systems, AAMAS '13, Saint Paul, MN, USA, May 6-10, 2013, pages 1283-1284, 2013. Google Scholar
  10. Grant Passmore, Simon Cruanes, Denis Ignatovich, Dave Aitken, Matt Bray, Elijah Kagan, Kostya Kanishev, Ewen Maclean, and Nicola Mometto. The imandra automated reasoning system (system description). In International Joint Conference on Automated Reasoning, pages 464-471. Springer, 2020. Google Scholar
  11. Grant Olney Passmore and Denis Ignatovich. Formal verification of financial algorithms. In 26th International Conference on Automated Deduction, Proceedings, volume 10395 of Lecture Notes in Computer Science, pages 26-41. Springer, 2017. Google Scholar
  12. Tobias Preis. Price-time priority and pro rata matching in an order book model of financial markets. In Econophysics of Order-driven Markets, pages 65-72. Springer, 2011. Google Scholar
  13. Suneel Sarswat and Abhishek Kr Singh. Formally verified trades in financial markets. In Formal Methods and Software Engineering - 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore, Singapore, March 1-3, 2021, Proceedings, volume 12531 of Lecture Notes in Computer Science, pages 217-232. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-63406-3_13.
  14. Securities Exchange Board of India (SEBI). Order in the matter of NSE Colocation, Apr 30, 2019. URL: https://www.sebi.gov.in/enforcement/orders/apr-2019/order-in-the-matter-of-nse-colocation_42880.html.
  15. The Coq Development Team. The coq reference manual, release 8.12.2, December 11 2020. URL: https://github.com/coq/coq/releases/download/V8.12.2/coq-8.12.2-reference-manual.pdf.
  16. U.S. Securities and Exchange Commision (SEC). SEC Charges UBS Subsidiary With Disclosure Violations and Other Regulatory Failures in Operating Dark Pool. https://www.sec.gov/news/pressrelease/2015-7.html, July, 2015.
  17. U.S. Securities and Exchange Commision (SEC). NYSE to Pay US Dollar 14 Million Penalty for Multiple Violations. https://www.sec.gov/news/press-release/2018-31, March 6, 2018.
  18. U.S. Securities and Exchange Commision (SEC). SEC Charges NYSE for Repeated Failures to Operate in Accordance With Exchange Rules. https://www.sec.gov/news/press-release/2014-87, May 1, 2014.
  19. Jim Woodcock, Peter Gorm Larsen, Juan Bicarregui, and John Fitzgerald. Formal methods: Practice and experience. ACM computing surveys (CSUR), 41(4):1-36, 2009. Google Scholar
  20. Peter R. Wurman, William E. Walsh, and Michael P. Wellman. Flexible double auctions for electronic commerce: theory and implementation. Decision Support Systems, 24(1):17-27, 1998. Google Scholar
  21. Junbeom Yoo, Taihyo Kim, Sungdeok Cha, Jang-Soo Lee, and Han Seong Son. A formal software requirements specification method for digital nuclear plant protection systems. Journal of Systems and Software, 74(1):73-83, 2005. Google Scholar
  22. Dengji Zhao, Dongmo Zhang, Md Khan, and Laurent Perrussel. Maximal matching for double auction. In Australasian Joint Conference on Artificial Intelligence, pages 516-525. Springer, 2010. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact