License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2021.28
URN: urn:nbn:de:0030-drops-139230
URL: https://drops.dagstuhl.de/opus/volltexte/2021/13923/
Go to the corresponding LIPIcs Volume Portal


Natarajan, Raja ; Sarswat, Suneel ; Singh, Abhishek Kr

Verified Double Sided Auctions for Financial Markets

pdf-format:
LIPIcs-ITP-2021-28.pdf (0.7 MB)


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.

BibTeX - Entry

@InProceedings{natarajan_et_al:LIPIcs.ITP.2021.28,
  author =	{Natarajan, Raja and Sarswat, Suneel and Singh, Abhishek Kr},
  title =	{{Verified Double Sided Auctions for Financial Markets}},
  booktitle =	{12th International Conference on Interactive Theorem Proving (ITP 2021)},
  pages =	{28:1--28:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-188-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{193},
  editor =	{Cohen, Liron and Kaliszyk, Cezary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/13923},
  URN =		{urn:nbn:de:0030-drops-139230},
  doi =		{10.4230/LIPIcs.ITP.2021.28},
  annote =	{Keywords: Double Sided Auction, Formal Verification, Financial Markets, Proof Assistant}
}

Keywords: Double Sided Auction, Formal Verification, Financial Markets, Proof Assistant
Collection: 12th International Conference on Interactive Theorem Proving (ITP 2021)
Issue Date: 2021
Date of publication: 21.06.2021
Supplementary Material: Software: https://github.com/suneel-sarswat/dsam archived at: https://archive.softwareheritage.org/swh:1:dir:94b9da19e3cfdb243bd47f1619a2901758fb1243


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI