{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,23]],"date-time":"2025-09-23T22:40:14Z","timestamp":1758667214436,"version":"3.44.0"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T00:00:00Z","timestamp":1750723200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T00:00:00Z","timestamp":1750723200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"name":"Walmart center for tech excellence at IISc","award":["CSIR Grant WMGT-23-0001"],"award-info":[{"award-number":["CSIR Grant WMGT-23-0001"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,9]]},"DOI":"10.1007\/s10817-025-09732-x","type":"journal-article","created":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T08:26:49Z","timestamp":1750753609000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Double Auctions: Formalization and Automated Checkers"],"prefix":"10.1007","volume":"69","author":[{"given":"Mohit","family":"Garg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"N.","family":"Raja","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Suneel","family":"Sarswat","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Abhishek Kr","family":"Singh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,6,24]]},"reference":[{"key":"9732_CR1","unstructured":"Natarajan, R., Sarswat, S., Singh, A.K.: Verified double sided auctions for financial markets. In: Cohen, L., Kaliszyk, C. (eds.) 12th International Conference on Interactive Theorem Proving, ITP 2021, Rome, Italy (Virtual Conference). LIPIcs, vol. 193, 28\u201312818 (2021)"},{"issue":"1","key":"9732_CR2","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/S0167-9236(98)00060-8","volume":"24","author":"PR Wurman","year":"1998","unstructured":"Wurman, P.R., Walsh, W.E., Wellman, M.P.: Flexible double auctions for electronic commerce: theory and implementation. Decision Support Systems 24(1), 17\u201327 (1998)","journal-title":"Decision Support Systems"},{"issue":"2","key":"9732_CR3","doi-asserted-by":"publisher","first-page":"434","DOI":"10.1016\/0022-0531(92)90091-U","volume":"56","author":"RP McAfee","year":"1992","unstructured":"McAfee, R.P.: A dominant strategy double auction. Journal of economic Theory 56(2), 434\u2013450 (1992)","journal-title":"Journal of economic Theory"},{"key":"9732_CR4","unstructured":"Niu, J., Parsons, S.: Maximizing matching in double-sided auctions. In: International Conference on Autonomous Agents and Multi-Agent Systems, AAMAS 2013, Saint Paul, MN, USA, pp. 1283\u20131284 (2013)"},{"key":"9732_CR5","doi-asserted-by":"crossref","unstructured":"Sarswat, S., Singh, A.K.: Formally verified trades in financial markets. In: Lin, S., Hou, Z., Mahony, B.P. (eds.) 22nd International Conference on Formal Engineering Methods, ICFEM 2020, Singapore. Lecture Notes in Computer Science, vol. 12531, pp. 217\u2013232 (2020)","DOI":"10.1007\/978-3-030-63406-3_13"},{"key":"9732_CR6","doi-asserted-by":"crossref","unstructured":"Zhao, D., Zhang, D., Khan, M., Perrussel, L.: Maximal matching for double auction. In: Li, J. (ed.) 23rd Australasian Joint Conference on Artificial Intelligence, AI 2010, Adelaide, Australia. Lecture Notes in Computer Science, vol. 6464, pp. 516\u2013525 (2010)","DOI":"10.1007\/978-3-642-17432-2_52"},{"key":"9732_CR7","unstructured":"Coq formalization of double aution. https:\/\/github.com\/ganitsutra\/DoubleAuctions\/tree\/master (2024)"},{"key":"9732_CR8","doi-asserted-by":"crossref","unstructured":"Passmore, G.O., Ignatovich, D.: Formal verification of financial algorithms. In: Moura, L. (ed.) 26th International Conference on Automated Deduction, CADE 26, Gothenburg, Sweden. Lecture Notes in Computer Science, vol. 10395, pp. 26\u201341 (2017)","DOI":"10.1007\/978-3-319-63046-5_3"},{"key":"9732_CR9","doi-asserted-by":"crossref","unstructured":"Passmore, G.O., Cruanes, S., Ignatovich, D., Aitken, D., Bray, M., Kagan, E., Kanishev, K., Maclean, E., Mometto, N.: The imandra automated reasoning system (system description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) 10th International Joint Conference Automated Reasoning, IJCAR (2) 2020, Paris, France. Lecture Notes in Computer Science, vol. 12167, pp. 464\u2013471 (2020)","DOI":"10.1007\/978-3-030-51054-1_30"},{"key":"9732_CR10","unstructured":"Garg, M., Sarswat, S.: The design and regulation of exchanges: A formal approach. In: Dawar, A., Guruswami, V. (eds.) 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2022, Chennai, India. LIPIcs, vol. 250, pp. 39\u201313921 (2022)"},{"key":"9732_CR11","doi-asserted-by":"crossref","unstructured":"Garg, M., Sarswat, S.: Efficient and verified continuous double auctions. In: Bj\u00f8rner, N.S., Heule, M., Voronkov, A. (eds.) LPAR 2024 Complementary Volume, Port Louis, Mauritius. Kalpa Publications in Computing, vol. 18, pp. 1\u201313 (2024)","DOI":"10.29007\/92jt"},{"key":"9732_CR12","doi-asserted-by":"crossref","unstructured":"Cervesato, I., Khan, S., Reis, G., Zunic, D.: Formalization of automated trading systems in a concurrent linear framework. In: Ehrhard, T., Fern\u00e1ndez, M., Paiva, V., Falco, L.T. (eds.) Joint International Workshop on Linearity & Trends in Linear Logic and Applications, Linearity-TLLA@FLoC 2018, Oxford, UK. EPTCS, vol. 292, pp. 1\u201314 (2018)","DOI":"10.4204\/EPTCS.292.0"},{"key":"9732_CR13","doi-asserted-by":"publisher","first-page":"330","DOI":"10.1007\/978-3-642-39320-4_23","volume-title":"Intelligent Computer Mathematics","author":"C Lange","year":"2013","unstructured":"Lange, C., Rowat, C., Kerber, M.: The formare project - formal mathematical reasoning in economics. In: Carette, J., Aspinall, D., Lange, C., Sojka, P., Windsteiger, W. (eds.) Intelligent Computer Mathematics, pp. 330\u2013334. Springer, Berlin, Heidelberg (2013)"},{"key":"9732_CR14","doi-asserted-by":"crossref","unstructured":"Lange, C., Caminati, M.B., Kerber, M., Mossakowski, T., Rowat, C., Wenzel, M., Windsteiger, W.: A qualitative comparison of the suitability of four theorem provers for basic auction theory. In: International Conference on Intelligent Computer Mathematics, pp. 200\u2013215 (2013). Springer","DOI":"10.1007\/978-3-642-39320-4_13"},{"key":"9732_CR15","unstructured":"Caminati, M.B., Kerber, M., Lange, C., Rowat, C.: VCG - combinatorial vickrey-clarke-groves auctions. Arch. Formal Proofs 2015 (2015)"},{"key":"9732_CR16","doi-asserted-by":"crossref","unstructured":"Caminati, M.B., Kerber, M., Lange, C., Rowat, C.: Sound auction specification and implementation. In: Roughgarden, T., Feldman, M., Schwarz, M. (eds.) Proceedings of the Sixteenth ACM Conference on Economics and Computation, EC 2015, Portland, OR, USA. ACM, pp. 547\u2013564 (2015)","DOI":"10.1145\/2764468.2764511"},{"key":"9732_CR17","doi-asserted-by":"crossref","unstructured":"Caminati, M.B., Kerber, M., Lange, C., Rowat, C.: Set theory or higher order logic to represent auction concepts in isabelle? In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) Intelligent Computer Mathematics - International Conference, CICM 2014, Coimbra, Portugal, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8543, pp. 236\u2013251 (2014)","DOI":"10.1007\/978-3-319-08434-3_18"},{"key":"9732_CR18","doi-asserted-by":"crossref","unstructured":"Tadjouddine, E.M., Guerin, F., Vasconcelos, W.W.: Abstracting and verifying strategy-proofness for auction mechanisms. In: Baldoni, M., Son, T.C., Riemsdijk, M.B., Winikoff, M. (eds.) 6th International Workshop on Declarative Agent Languages and Technologies VI, DALT 2008, Estoril, Portugal. Lecture Notes in Computer Science, vol. 5397, pp. 197\u2013214 (2008)","DOI":"10.1007\/978-3-540-93920-7_13"},{"key":"9732_CR19","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1145\/3167100","volume-title":"7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018","author":"C Kaliszyk","year":"2018","unstructured":"Kaliszyk, C., Parsert, J.: Formal microeconomic foundations and the first welfare theorem. In: Andronick, J., Felty, A.P. (eds.) 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, pp. 91\u2013101. Los Angeles, CA, USA (2018)"},{"key":"9732_CR20","doi-asserted-by":"crossref","unstructured":"Echenim, M., Peltier, N.: The binomial pricing model in finance: A formalization in isabelle. In: Moura, L. (ed.) Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings. Lecture Notes in Computer Science, vol. 10395, pp. 546\u2013562 (2017)","DOI":"10.1007\/978-3-319-63046-5_33"},{"key":"9732_CR21","doi-asserted-by":"crossref","unstructured":"Roux, S.L.: Acyclic preferences and existence of sequential nash equilibria: A formal and constructive equivalence. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2009, Munich, Germany. Lecture Notes in Computer Science, vol. 5674, pp. 293\u2013309 (2009)","DOI":"10.1007\/978-3-642-03359-9_21"},{"key":"9732_CR22","doi-asserted-by":"crossref","unstructured":"Roux, S.L., Martin-Dorel, \u00c9., Smaus, J.: An existence theorem of nash equilibrium in coq and isabelle. In: Bouyer, P., Orlandini, A., Pietro, P.S. (eds.) Proceedings Eighth International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2017, Roma, Italy, 20-22 September 2017. EPTCS, vol. 256, pp. 46\u201360 (2017)","DOI":"10.4204\/EPTCS.256.4"},{"key":"9732_CR23","unstructured":"Pomeret-Coquot, P., Fargier, H., Martin-Dorel, \u00c9.: Bel-games: A formal theory of games of incomplete information based on belief functions in the coq proof assistant. In: Naumowicz, A., Thiemann, R. (eds.) 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Bia\u0142ystok, Poland. LIPIcs, vol. 268, pp. 25\u201312519 (2023)"},{"key":"9732_CR24","doi-asserted-by":"crossref","unstructured":"Parsert, J., Kaliszyk, C.: Towards formal foundations for game theory. In: Avigad, J., Mahboubi, A. (eds.) Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, Proceedings. Lecture Notes in Computer Science, vol. 10895, pp. 495\u2013503 (2018)","DOI":"10.1007\/978-3-319-94821-8_29"},{"key":"9732_CR25","unstructured":"Gammie, P.: Stable matching. Arch. Formal Proofs 2016 (2016)"},{"key":"9732_CR26","doi-asserted-by":"crossref","unstructured":"Hamid, N.A., Castleberry, C.: Formally certified stable marriages. In: Cunningham, H.C., Ruth, P., Kraft, N.A. (eds.) Proceedings of the 48th Annual Southeast Regional Conference, 2010, Oxford, MS, USA, April 15-17, 2010. ACM, p. 34 (2010)","DOI":"10.1145\/1900008.1900056"},{"issue":"2","key":"9732_CR27","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/s10817-024-09700-x","volume":"68","author":"T Nipkow","year":"2024","unstructured":"Nipkow, T.: Gale-shapley verified. J. Autom. Reason. 68(2), 12 (2024)","journal-title":"J. Autom. Reason."},{"key":"9732_CR28","unstructured":"Matthieu Sozeau: Equations - a function definition plugin. https:\/\/github.com\/mattam82\/Coq-Equations\/tree\/main (2022)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09732-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-025-09732-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09732-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,23]],"date-time":"2025-09-23T22:02:57Z","timestamp":1758664977000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-025-09732-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,24]]},"references-count":28,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9]]}},"alternative-id":["9732"],"URL":"https:\/\/doi.org\/10.1007\/s10817-025-09732-x","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2025,6,24]]},"assertion":[{"value":"10 November 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 June 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 June 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"17"}}