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.FSTTCS.2022.39
URN: urn:nbn:de:0030-drops-174318
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/17431/
Go to the corresponding LIPIcs Volume Portal

Garg, Mohit ; Sarswat, Suneel

The Design and Regulation of Exchanges: A Formal Approach

pdf-format:
LIPIcs-FSTTCS-2022-39.pdf (1 MB)

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.

BibTeX - Entry

@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/opus/volltexte/2022/17431},
  URN =		{urn:nbn:de:0030-drops-174318},
  doi =		{10.4230/LIPIcs.FSTTCS.2022.39},
  annote =	{Keywords: Double Auctions, Formal Specification and Verification, Financial Markets}
}

Keywords: Double Auctions, Formal Specification and Verification, Financial Markets
Collection: 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)
Issue Date: 2022
Date of publication: 14.12.2022
Supplementary Material: Other (Coq-Formalization): https://github.com/suneel-sarswat/cda

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