LIPIcs.ITP.2021.28.pdf
- Filesize: 0.7 MB
- 18 pages
Document
Verified Double Sided Auctions for Financial Markets
Authors
-
Part of:
Volume:
12th International Conference on Interactive Theorem Proving (ITP 2021)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2021-06-21
File
Document Identifiers
Acknowledgements
We wish to thank Mohit Garg for his generous contribution to this work.
Cite AsGet BibTex
Raja Natarajan, Suneel Sarswat, and Abhishek Kr Singh. Verified Double Sided Auctions for Financial Markets. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 28:1-28:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.ITP.2021.28
https://doi.org/10.4230/LIPIcs.ITP.2021.28
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 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.
Subject Classification
ACM Subject Classification
- Information systems → Online auctions
- Software and its engineering → Formal software verification
- Theory of computation → Algorithmic mechanism design
- Theory of computation → Computational pricing and auctions
- Theory of computation → Program verification
- Theory of computation → Automated reasoning
Keywords
- Double Sided Auction
- Formal Verification
- Financial Markets
- Proof Assistant
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Iliano Cervesato, Sharjeel Khan, Giselle Reis, and Dragisa Zunic. 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.
-
Cezary Kaliszyk and Julian Parsert. Formal microeconomic foundations and the first welfare theorem. In Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 91-101. ACM, 2018.
-
Stéphane Le Roux. Acyclic preferences and existence of sequential nash equilibria: a formal and constructive equivalence. In International Conference on Theorem Proving in Higher Order Logics, pages 293-309. Springer, 2009.
-
R Preston McAfee. A dominant strategy double auction. Journal of economic Theory, 56(2):434-450, 1992.
- Raja Natarajan, Suneel Sarswat, and Abhishek Kr Singh. Verified double sided auctions for financial markets, 2021. URL: http://arxiv.org/abs/2104.08437.
-
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.
-
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.
- Suneel Sarswat and Abhishek Kr Singh. Formally verified trades in financial markets. In Shang-Wei Lin, Zhe Hou, and Brendan Mahoney, editors, 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.
-
Matthieu Sozeau and Cyprien Mangin. Equations reloaded: High-level dependently-typed functional programming and proving in coq. Proceedings of the ACM on Programming Languages, 3(ICFP):1-29, 2019.
-
Suneel Sarswat. Coq formalization of mdsa. ěrb+https://github.com/suneel-sarswat/dsam+.
-
Emmanuel M. Tadjouddine, Frank Guerin, and Wamberto Weber Vasconcelos. Abstracting and verifying strategy-proofness for auction mechanisms. In DALT, volume 5397 of Lecture Notes in Computer Science, pages 197-214. Springer, 2008.
-
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.
-
Dengji Zhao, Dongmo Zhang, Md Khan, and Laurent Perrussel. Maximal matching for double auction. In Australasian Conference on Artificial Intelligence, volume 6464 of Lecture Notes in Computer Science, pages 516-525. Springer, 2010.