金融市场交易的正式验证

订单发送、清算和结算TC）。References1 SEC因纽约证券交易所屡次未能按照交易所规则运作而向其收取费用。2纽约证券交易所因多次违规支付1400万美元罚款。NSE共定位问题为3级。4 Coq拍卖形式化。https://github.com/suneel-sarswat/auction.5Coq标准库。https://coq.inria.fr/library/.6Marco B.Caminati、Manfred Kerber、Christoph Lange 0002和Colin Rowat。声音拍卖规范和实施。《第十六届ACM经济与计算会议论文集》，编辑Tim Rawgarden、Michal Feldman和Michael Schwarz，EC’15，波特兰，或美国，2015年6月15-19日，第547-564页。ACM，2015.7丹尼尔·弗里德曼。双重拍卖市场制度：一项调查。《双重拍卖市场：制度、理论和证据》，14:3–251993.8托马斯·亨辛格、兰吉特·贾拉、鲁帕克·马朱姆达尔和格雷戈伊尔·萨特尔。使用blast进行软件验证。在软件模型检查国际SPIN研讨会上，第235–239页。Springer，2003.9 J.R.Burch、E.M.Clarke和K.L.McMillan。使用符号模型检查进行时序电路验证。在第27届设计自动化会议上，第46–51页，1990.10格温·克莱因、凯文·埃尔芬斯通、格诺特·海泽、琼·安德罗尼克、大卫·科克、菲利普·德林、达米卡·埃尔卡杜威、凯·恩格尔哈特、拉法·科兰斯基、迈克尔·诺里斯等。sel4：操作系统内核的正式验证。ACM SIGOPS第22届操作系统原理研讨会论文集，第207-220页。ACM，2009.11 Christoph Lange、Marco B Caminati、Manfred Kerber、Till Mossakowski、Colin Rowat、Makarius Wenzel和Wolfgang Windsteiger。四个定理证明器对基本拍卖理论适用性的定性比较。智能计算机数学国际会议，第200–215页。斯普林格，2013.12泽维尔·勒罗伊。正式验证的编译器后端。

《自动推理杂志》，43（4）：3632009.13 R Preston McAfee。双重拍卖的主导策略。《经济理论杂志》，56（2）：434-4501992.14牛晋中和西蒙·帕森斯。在双边拍卖中最大化匹配。InMaria L.Gini、Onn Shehory、Takayuki Ito和Catholijn M.Jonker，《自主智能体和多智能体系统国际会议》编辑，AAMAS’13，美国明尼苏达州圣保罗，2013年5月6日至10日，第1283–1284页。15 Grant Olney Passmore和Denis Ignatovich。财务算法的形式验证。2017年8月6日至11日，瑞典哥德堡，第26届自动扣除国际会议，自动扣除-CADE 26-26编辑Leonardo de Moura，《计算机科学讲稿》第10395卷，第26-41页。斯普林格，2017.16艾曼纽尔·塔朱丁（Emmanuel M.Tadjouddine）、弗兰克·盖林（Frank Guerin）和沃姆贝托·韦伯·瓦康塞洛斯（Wamberto Weber Vasconcelos）。抽象并验证拍卖机制的策略证明性。在Matteo Baldoni、Tran Cao Son、M.Birna van Riemsdijk和Michael Winiko Off中，DALT编辑，《计算机科学讲师》第5397卷，第197-214页。斯普林格，2008.17彼得·R·沃尔曼、威廉·E·沃尔什和迈克尔·P·威尔曼。电子商务中的灵活双重拍卖：理论与实现。决策支持系统，24（1）：17–271998。