Search Results

Documents authored by Sarswat, Suneel

Document
DOI: 10.4230/LIPIcs.FSTTCS.2022.39
The Design and Regulation of Exchanges: A Formal Approach

Authors: Mohit Garg and Suneel Sarswat

Published in: LIPIcs, Volume 250, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)

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.
Cite as

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)

Copy BibTex To Clipboard

@InProceedings{garg_et_al:LIPIcs.FSTTCS.2022.39,
  author =	{Garg, Mohit and Sarswat, Suneel},
  title =	{{The Design and Regulation of Exchanges: A Formal Approach}},
  booktitle =	{42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)},
  pages =	{39:1--39:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-261-7},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{250},
  editor =	{Dawar, Anuj and Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2022.39},
  URN =		{urn:nbn:de:0030-drops-174318},
  doi =		{10.4230/LIPIcs.FSTTCS.2022.39},
  annote =	{Keywords: Double Auctions, Formal Specification and Verification, Financial Markets}
}
Document
DOI: 10.4230/LIPIcs.ITP.2021.28
Verified Double Sided Auctions for Financial Markets

Authors: Raja Natarajan, Suneel Sarswat, and Abhishek Kr Singh

Published in: LIPIcs, Volume 193, 12th International Conference on Interactive Theorem Proving (ITP 2021)

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.
Cite as

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)

Copy BibTex To Clipboard

@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/entities/document/10.4230/LIPIcs.ITP.2021.28},
  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}
}
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