Creative Commons Attribution 4.0 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: https://drops.dagstuhl.de/opus/volltexte/2022/17431/
Garg, Mohit ; Sarswat, Suneel
The Design and Regulation of Exchanges: A Formal Approach
| pdf-format: |
|
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 | |
| Seminar: | 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 |
