{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,24]],"date-time":"2025-09-24T09:41:48Z","timestamp":1758706908267},"publisher-location":"Cham","reference-count":20,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319630458"},{"type":"electronic","value":"9783319630465"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-63046-5_3","type":"book-chapter","created":{"date-parts":[[2017,7,10]],"date-time":"2017-07-10T13:34:07Z","timestamp":1499693647000},"page":"26-41","source":"Crossref","is-referenced-by-count":15,"title":["Formal Verification of Financial Algorithms"],"prefix":"10.1007","author":[{"given":"Grant Olney","family":"Passmore","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Denis","family":"Ignatovich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,11]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Bahr, P., Berthold, J., Elsman, M.: Certified symbolic management of financial multi-party contracts. In: 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, pp. 315\u2013327 (2015)","DOI":"10.1145\/2784731.2784747"},{"issue":"4","key":"3_CR2","first-page":"409","volume":"5","author":"WR Bevier","year":"1989","unstructured":"Bevier, W.R., Hunt, W.A., Moore, J.S., Young, W.D.: Special issue on system verification. J. Autom. Reasoning 5(4), 409\u2013530 (1989)","journal-title":"J. Autom. Reasoning"},{"key":"3_CR3","unstructured":"Buterin, V.: Ethereum: a next-generation smart contract and decentralized application platform (2014). https:\/\/github.com\/ethereum\/wiki\/wiki\/White-Paper"},{"issue":"9","key":"3_CR4","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"L Moura De","year":"2011","unstructured":"De Moura, L., Bj\u00f8rner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69\u201377 (2011)","journal-title":"Commun. ACM"},{"key":"3_CR5","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780195144703.001.0001","volume-title":"Trading and Exchanges: Market Microstructure for Practitioners","author":"L Harris","year":"2002","unstructured":"Harris, L.: Trading and Exchanges: Market Microstructure for Practitioners. Oxford University Press, Oxford (2002)"},{"key":"3_CR6","unstructured":"Hunt Jr., W.A., Krug, R.B., Moore, J.: Integrating nonlinear arithmetic into ACL2. In: Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (2004)"},{"key":"3_CR7","unstructured":"Ignatovich, D.A., Passmore, G.O.: Case Study: 2015 SEC Fine Against UBS ATS. Aesthetic Integration, Ltd., Technical Whitepaper (2015)"},{"key":"3_CR8","unstructured":"Ignatovich, D.A., Passmore, G.O.: Creating Safe and Fair Markets. Aesthetic Integration, Ltd., Technical Whitepaper (2015)"},{"key":"3_CR9","unstructured":"Ignatovich, D.A., Passmore, G.O.: Transparent Order Priority and Pricing. Aesthetic Integration, Ltd., Technical Whitepaper (2015)"},{"key":"3_CR10","unstructured":"Ignatovich, D.A., Passmore, G.O.: Comment on SEC Reg ATS-N: The Precise Specification Standard, February 2016. https:\/\/www.sec.gov\/comments\/s7-23-15\/s72315-24.pdf"},{"key":"3_CR11","volume-title":"Computer-Aided Reasoning: An Approach","author":"M Kaufmann","year":"2000","unstructured":"Kaufmann, M., Moore, J.S., Manolios, P.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Norwell (2000)"},{"key":"3_CR12","unstructured":"Leroy, X., Doligez, D., Frisch, A., Garrigue, J., R\u00e9my, D., Vouillon, J.: The OCaml system (release 4.04): Documentation and user\u2019s manual. INRIA (2017)"},{"key":"3_CR13","doi-asserted-by":"crossref","unstructured":"Li, W., Passmore, G.O., Paulson, L.C.: Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle\/HOL. J. Autom. Reasoning (2017)","DOI":"10.1007\/s10817-017-9424-6"},{"key":"3_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-642-36675-8_2","volume-title":"Automated Reasoning and Mathematics","author":"L Moura","year":"2013","unstructured":"Moura, L., Passmore, G.O.: The strategy challenge in SMT solving. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS, vol. 7788, pp. 15\u201344. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-36675-8_2"},{"key":"3_CR15","unstructured":"Myreen, M.O.: Formal verification of machine-code programs. Ph.D. thesis, University of Cambridge (2009)"},{"key":"3_CR16","unstructured":"Passmore, G.O.: Combined decision procedures for nonlinear arithmetics, real and complex. Ph.D. thesis, University of Edinburgh (2011)"},{"issue":"9","key":"3_CR17","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1145\/357766.351267","volume":"35","author":"S Peyton Jones","year":"2000","unstructured":"Peyton Jones, S., Eber, J.M., Seward, J.: Composing contracts: an adventure in financial engineering (functional pearl). SIGPLAN Not. 35(9), 280\u2013292 (2000). http:\/\/doi.acm.org\/10.1145\/357766.351267","journal-title":"SIGPLAN Not."},{"key":"3_CR18","unstructured":"US Securities and Exchange Commission: Regulation National Market System (Reg NMS) (2005). https:\/\/www.sec.gov\/rules\/final\/34-51808.pdf"},{"key":"3_CR19","unstructured":"US Securities and Exchange Commission: Regulation Alternative Trading Systems (Reg ATS) (2015). https:\/\/www.sec.gov\/rules\/proposed\/2015\/34-76474.pdf"},{"key":"3_CR20","unstructured":"Wood, G.: Ethereum: a secure decentralised generalised transaction ledger (2014). http:\/\/gavwood.com\/paper.pdf"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 26"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-63046-5_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,25]],"date-time":"2024-06-25T10:13:39Z","timestamp":1719310419000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-63046-5_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319630458","9783319630465"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-63046-5_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}