2026-07-22T00:13:45Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:17431 2024-03-06T10:59:44Z ddc:004 open_access

The Design and Regulation of Exchanges: A Formal Approach Garg, Mohit Sarswat, Suneel Double Auctions Formal Specification and Verification Financial Markets 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Mohit Garg and Suneel Sarswat 2022 Is Part Of LIPIcs, Volume 250, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSTTCS.2022.39 urn:nbn:de:0030-drops-174318 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2022.39 eng https://creativecommons.org/licenses/by/4.0/legalcode