{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,27]],"date-time":"2026-03-27T11:17:00Z","timestamp":1774610220263,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":43,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662639573","type":"print"},{"value":"9783662639580","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-662-63958-0_13","type":"book-chapter","created":{"date-parts":[[2021,9,16]],"date-time":"2021-09-16T14:04:04Z","timestamp":1631801044000},"page":"149-161","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":27,"title":["Formal Analysis of Composable DeFi Protocols"],"prefix":"10.1007","author":[{"given":"Palina","family":"Tolmach","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yi","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shang-Wei","family":"Lin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yang","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,9,17]]},"reference":[{"key":"13_CR1","unstructured":"Harvest Finance (2020). https:\/\/harvest.finance\/. Accessed 12 Oct 2020"},{"key":"13_CR2","unstructured":"Introduction to Yearn - yearn.finance (2020). https:\/\/docs.yearn.finance\/. Accessed 12 Nov 2020"},{"key":"13_CR3","unstructured":"Whitepaper - Balancer (2020). https:\/\/balancer.finance\/whitepaper\/. Accessed 12 Oct 2020"},{"key":"13_CR4","unstructured":"Adams, H., Zinsmeister, N., Robinson, D.: Uniswap v2 Core Whitepaper (2020). https:\/\/uniswap.org\/whitepaper.pdf. Accessed 12 Oct 2020"},{"key":"13_CR5","doi-asserted-by":"crossref","unstructured":"Angeris, G., Kao, H.T., Chiang, R., Noyes, C., Chitra, T.: An analysis of uniswap markets (2020). https:\/\/arxiv.org\/abs\/1911.03380","DOI":"10.21428\/58320208.c9738e64"},{"key":"13_CR6","unstructured":"Bartoletti, M., Chiang, J.H., Lluch-Lafuente, A.: SOK: lending pools in decentralized finance (2020). https:\/\/arxiv.org\/abs\/2012.13230"},{"key":"13_CR7","unstructured":"Bernardi, T., et al.: WIP: finding bugs automatically in smart contracts with parameterized invariants (2020). https:\/\/www.certora.com\/pubs\/sbc2020.pdf. Accessed 14 July 2020"},{"key":"13_CR8","doi-asserted-by":"publisher","unstructured":"Chen, W., Zhang, T., Chen, Z., Zheng, Z., Lu, Y.: Traveling the token world: a graph analysis of Ethereum ERC20 token ecosystem. In: Proceedings of The Web Conference 2020. WWW 2020, pp. 1411\u20131421. ACM (2020). https:\/\/doi.org\/10.1145\/3366423.3380215","DOI":"10.1145\/3366423.3380215"},{"key":"13_CR9","volume-title":"Model Checking","author":"EM Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"13_CR10","unstructured":"Coingape: DeFi success story continues as TVL peaks yet again; hits \\$12 billion (2020). https:\/\/coinmarketcap.com\/ru\/headlines\/news\/defi-success-story-continues-as-tvl-peaks-yet-again-hits-12-billion. Accessed 18 Nov 2020"},{"key":"13_CR11","unstructured":"Daian, P., et al.: Flash boys 2.0: Frontrunning, transaction reordering, and consensus instability in decentralized exchanges (2019). https:\/\/arxiv.org\/abs\/1904.05234"},{"key":"13_CR12","unstructured":"Egorov, M.: StableSwap - efficient mechanism for Stablecoin liquidity \u2014 Curve. fi Whitepaper (2020). https:\/\/www.curve.fi\/stableswap-paper.pdf. Accessed 18 Nov 18 2020"},{"key":"13_CR13","unstructured":"Finance, H.: Harvest Flashloan Economic Attack Post-Mortem (2020). https:\/\/medium.com\/harvest-finance\/harvest-flashloan-economic-attack-post-mortem-3cf900d65217. Accessed 18 Nov 2020"},{"key":"13_CR14","unstructured":"Foxley, W.: DeFi project Akropolis drained of \\$2m in DAI (2020). https:\/\/www.coindesk.com\/defi-project-akropolis-token-pool-drained. Accessed 14 Nov 2020"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Grossman, S., et al.: Online detection of effectively callback free objects with applications to smart contracts. Proc. ACM Program. Lang. pp. 1\u201328 (2017). https:\/\/doi.org\/10.1145\/3158136","DOI":"10.1145\/3158136"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Gudgeon, L., Perez, D., Harz, D., Livshits, B., Gervais, A.: The decentralized financial crisis (2020). https:\/\/arxiv.org\/abs\/2002.08099","DOI":"10.1109\/CVCBT50464.2020.00005"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Gudgeon, L., Werner, S.M., Perez, D., Knottenbelt, W.J.: DeFi protocols for loanable funds: interest rates, liquidity and market efficiency (2020). https:\/\/arxiv.org\/abs\/2006.13922","DOI":"10.1145\/3419614.3423254"},{"key":"13_CR18","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. International Series on Computer Science, Prentice-Hall (1985)"},{"key":"13_CR19","unstructured":"Kao, H.T., Chitra, T., Chiang, R., Morrow, J.: An Analysis of the Market Risk to Participants in the Compound Protocol (2020). https:\/\/scfab.github.io\/2020\/FAB2020_p5.pdf. Accessed 18 Nov 2020"},{"key":"13_CR20","doi-asserted-by":"publisher","unstructured":"Klages-Mundt, A., Harz, D., Gudgeon, L., Liu, J.Y., Minca, A.: Stablecoins 2.0. In: Proceedings of the 2nd ACM Conference on Advances in Financial Technologies, October 2020. https:\/\/doi.org\/10.1145\/3419614.3423261","DOI":"10.1145\/3419614.3423261"},{"key":"13_CR21","unstructured":"Leshner, R., Hayes, G.: Compound: The Money Market Protocol \u2014 Whitepaper (2020). https:\/\/compound.finance\/documents\/Compound.Whitepaper.pdf. Accessed 18 Nov 2020"},{"key":"13_CR22","doi-asserted-by":"publisher","unstructured":"Li, X., Su, C., Xiong, Y., Huang, W., Wang, W.: Formal verification of BNB smart contract. In: Proceedings of the BIGCOM, pp. 74\u201378, August 2019. https:\/\/doi.org\/10.1109\/BIGCOM.2019.00021","DOI":"10.1109\/BIGCOM.2019.00021"},{"key":"13_CR23","doi-asserted-by":"publisher","unstructured":"Lin, S., Andre, E., Liu, Y., Sun, J., Dong, J.: Learning assumptions for compositional verification of timed systems. IEEE Trans. Software Eng. (02), 137\u2013153 (2014). https:\/\/doi.org\/10.1109\/TSE.2013.57","DOI":"10.1109\/TSE.2013.57"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-642-32759-9_24","volume-title":"FM 2012: Formal Methods","author":"S-W Lin","year":"2012","unstructured":"Lin, S.-W., Liu, Y., Sun, J., Dong, J.S., Andr\u00e9, \u00c9.: Automatic compositional verification of timed systems. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 272\u2013276. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_24"},{"key":"13_CR25","doi-asserted-by":"publisher","unstructured":"Lin, S.W., Sun, J., Nguyen, T.K., Liu, Y., Dong, J.S.: Interpolation guided compositional verification. In: Proceedings of the 30th IEEE\/ACM International Conference on Automated Software Engineering. ASE 2015, pp. 65\u201374. IEEE Press (2015). https:\/\/doi.org\/10.1109\/ASE.2015.33","DOI":"10.1109\/ASE.2015.33"},{"key":"13_CR26","unstructured":"Liu, B., Szalachowski, P.: A first look into DeFi oracles (2020). https:\/\/arxiv.org\/abs\/2005.04377"},{"key":"13_CR27","doi-asserted-by":"publisher","unstructured":"Liu, C., Liu, H., Cao, Z., Chen, Z., Chen, B., Roscoe, B.: ReGuard: finding reentrancy bugs in smart contracts. In: Proceedings of the 40th International Conference on Software Engineering: Companion Proceedings, pp. 65\u201368. ACM (2018). https:\/\/doi.org\/10.1145\/3183440.3183495","DOI":"10.1145\/3183440.3183495"},{"key":"13_CR28","doi-asserted-by":"publisher","unstructured":"Liu, Y., Sun, J., Dong, J.S.: Pat 3: An extensible architecture for building multi-domain model checkers. In: 2011 IEEE 22nd International Symposium on Software Reliability Engineering, pp. 190\u2013199 (2011). https:\/\/doi.org\/10.1109\/ISSRE.2011.19","DOI":"10.1109\/ISSRE.2011.19"},{"key":"13_CR29","unstructured":"Moin, A., Sirer, E.G., Sekniqi, K.: A classification framework for stablecoin designs (2019). https:\/\/arxiv.org\/abs\/1910.10098"},{"key":"13_CR30","unstructured":"Perez, D., Werner, S.M., Xu, J., Livshits, B.: Liquidations: DeFi on a knife-edge (2020). https:\/\/arxiv.org\/abs\/2009.13235"},{"key":"13_CR31","unstructured":"Pulse, D.: DeFi status report post-black thursday (2020). https:\/\/defipulse.com\/blog\/defi-status-report-black-thursday. Accessed 18 Nov 2020"},{"key":"13_CR32","unstructured":"Qin, K., Zhou, L., Livshits, B., Gervais, A.: Attacking the DeFi ecosystem with flash loans for fun and profit (2020). https:\/\/arxiv.org\/abs\/2003.03810"},{"key":"13_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-030-05764-0_4","volume-title":"Smart Blockchain","author":"M Qu","year":"2018","unstructured":"Qu, M., Huang, X., Chen, X., Wang, Y., Ma, X., Liu, D.: Formal verification of smart contracts from the perspective of concurrency. In: Qiu, M. (ed.) SmartBlock 2018. LNCS, vol. 11373, pp. 32\u201343. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-05764-0_4"},{"key":"13_CR34","unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall (1997). iSBN 0-13-674409-5"},{"key":"13_CR35","doi-asserted-by":"publisher","unstructured":"Samreen, N., Alalfi, M.H.: Reentrancy vulnerability identification in Ethereum smart contracts. In: 2020 IEEE International Workshop on Blockchain Oriented Software Engineering (IWBOSE), pp. 22\u201329 (2020). https:\/\/doi.org\/10.1109\/IWBOSE50093.2020.9050260","DOI":"10.1109\/IWBOSE50093.2020.9050260"},{"key":"13_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1007\/978-3-642-02658-4_59","volume-title":"Computer Aided Verification","author":"J Sun","year":"2009","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709\u2013714. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_59"},{"key":"13_CR37","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-540-88479-8_22","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation","author":"J Sun","year":"2008","unstructured":"Sun, J., Liu, Y., Dong, J.S.: Model checking CSP revisited: introducing a process analysis toolkit. In: Margaria, T., Steffen, B. (eds.) ISoLA 2008. CCIS, vol. 17, pp. 307\u2013322. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-88479-8_22"},{"key":"13_CR38","doi-asserted-by":"publisher","unstructured":"Sun, J., Liu, Y., Dong, J.S., Chen, C.: Integrating specification and programs for system modeling and verification. In: Proceedings of the 2009 Third IEEE International Symposium on Theoretical Aspects of Software Engineering, pp. 127\u2013135 (2009). https:\/\/doi.org\/10.1109\/TASE.2009.32","DOI":"10.1109\/TASE.2009.32"},{"key":"13_CR39","doi-asserted-by":"publisher","unstructured":"Tolmach, P., Li, Y., Lin, S.-W., Liu, Y., Li, Z.: A survey of smart contract formal specification and verification. ACM Comput. Surv. 54(7), 38 p. (2021). Article no. 148. https:\/\/doi.org\/10.1145\/3464421","DOI":"10.1145\/3464421"},{"key":"13_CR40","unstructured":"Totle: Building with Money Legos (2020). https:\/\/medium.com\/totle\/building-with-money-legos-ab63a58ae764. Accessed 17 Nov 2020"},{"key":"13_CR41","unstructured":"Vogelsteller, F., Buterin, V.: ERC-20 token standard (2015). https:\/\/eips.ethereum.org\/EIPS\/eip-20. Accessed 14 July 2020"},{"key":"13_CR42","doi-asserted-by":"crossref","unstructured":"Wang, D., et al.: Towards understanding flash loan and its applications in DeFi ecosystem (2020). https:\/\/arxiv.org\/abs\/2010.12252","DOI":"10.1145\/3457977.3460301"},{"issue":"4","key":"13_CR43","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1592434.1592436","volume":"41","author":"J Woodcock","year":"2009","unstructured":"Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: practice and experience. ACM Comput. Surv. 41(4), 1\u201336 (2009). https:\/\/doi.org\/10.1145\/1592434.1592436","journal-title":"ACM Comput. Surv."}],"container-title":["Lecture Notes in Computer Science","Financial Cryptography and Data Security. FC 2021 International Workshops"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-63958-0_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,16]],"date-time":"2021-09-16T14:08:12Z","timestamp":1631801292000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-63958-0_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783662639573","9783662639580"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-63958-0_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"17 September 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Financial Cryptography and Data Security","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 March 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fc2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/fc21.ifca.ai\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}