{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T18:00:44Z","timestamp":1773511244961,"version":"3.50.1"},"reference-count":79,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2024,1,25]],"date-time":"2024-01-25T00:00:00Z","timestamp":1706140800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,25]],"date-time":"2024-01-25T00:00:00Z","timestamp":1706140800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2024,6]]},"DOI":"10.1007\/s10270-023-01143-z","type":"journal-article","created":{"date-parts":[[2024,1,25]],"date-time":"2024-01-25T13:50:43Z","timestamp":1706190643000},"page":"657-693","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["A refinement-based approach to safe smart contract deployment and evolution"],"prefix":"10.1007","volume":"23","author":[{"given":"Pedro","family":"Antonino","sequence":"first","affiliation":[]},{"given":"Juliandson","family":"Ferreira","sequence":"additional","affiliation":[]},{"given":"Augusto","family":"Sampaio","sequence":"additional","affiliation":[]},{"given":"A. W.","family":"Roscoe","sequence":"additional","affiliation":[]},{"given":"Filipe","family":"Arruda","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,1,25]]},"reference":[{"key":"1143_CR1","unstructured":"AMD SEV-SNP: Strengthening VM isolation with integrity protection and more (2020)"},{"key":"1143_CR2","unstructured":"Adhikari, C.: Secure framework for healthcare data management using ethereum-based blockchain technology. In: 2017 Undergraduate Research and Scholarship Conference (2017)"},{"key":"1143_CR3","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/978-3-030-61467-6_2","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Applications","author":"W Ahrendt","year":"2020","unstructured":"Ahrendt, W., Bubel, R.: Functional verification of smart contracts via strong data integrity. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Applications, pp. 9\u201324. Springer, Cham (2020)"},{"key":"1143_CR4","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-030-31517-7_16","volume-title":"Fundamentals of Software Engineering","author":"W Ahrendt","year":"2019","unstructured":"Ahrendt, W., Bubel, R., Ellul, J., Pace, G.J., Pardo, R., Rebiscoul, V., Schneider, G.: Verification of smart contract business logic. In: Hojjat, H., Massink, M. (eds.) Fundamentals of Software Engineering, pp. 228\u2013243. Springer, Cham (2019)"},{"key":"1143_CR5","doi-asserted-by":"publisher","first-page":"840","DOI":"10.1109\/TDSC.2016.2616861","volume":"15","author":"NZ Aitzhan","year":"2016","unstructured":"Aitzhan, N.Z., Svetinovic, D.: Security and privacy in decentralized energy trading through multi-signatures, blockchain and anonymous messaging streams. IEEE Trans. Dependable Secure Comput. 15, 840\u2013852 (2016)","journal-title":"IEEE Trans. Dependable Secure Comput."},{"key":"1143_CR6","doi-asserted-by":"publisher","first-page":"90839","DOI":"10.1109\/ACCESS.2023.3308850","volume":"11","author":"P Antonino","year":"2023","unstructured":"Antonino, P., Derek, A., Wo\u0142oszyn, W.A.: Flexible remote attestation of pre-SNP SEV VMs using SGX enclaves. IEEE Access 11, 90839\u201390856 (2023)","journal-title":"IEEE Access"},{"key":"1143_CR7","doi-asserted-by":"crossref","unstructured":"Antonino, P., Ferreira, J., Sampaio, A., Roscoe, A.W.: Specification is law: safe creation and upgrade of ethereum smart contracts. In: Schlingloff, B.H., Chai, M. (eds.) Software Engineering and Formal Methods\u201420th International Conference, SEFM 2022, Berlin, Germany, September 26\u201330, 2022, Proceedings, volume 13550 of Lecture Notes in Computer Science, pp. 227\u2013243. Springer (2022)","DOI":"10.1007\/978-3-031-17108-6_14"},{"key":"1143_CR8","doi-asserted-by":"crossref","unstructured":"Antonino, P., Roscoe, A.W.: Formalising and verifying smart contracts with solidifier: a bounded model checker for solidity (2020)","DOI":"10.1145\/3412841.3442051"},{"key":"1143_CR9","doi-asserted-by":"crossref","unstructured":"Antonino, P., Roscoe, A.W.: Solidifier: bounded model checking solidity using lazy contract deployment and precise memory modelling. In: Proceedings of the 36th Annual ACM Symposium on Applied Computing, SAC\u201921, pp. 1788\u20131797 (2021)","DOI":"10.1145\/3412841.3442051"},{"key":"1143_CR10","doi-asserted-by":"crossref","unstructured":"Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on ethereum smart contracts (sok). In: POST 2017, pp. 164\u2013186. Springer (2017)","DOI":"10.1007\/978-3-662-54455-6_8"},{"key":"1143_CR11","doi-asserted-by":"crossref","unstructured":"Azzopardi, S., Ellul, J., Pace, G.J.: Monitoring smart contracts: contractlarva and open challenges beyond. In: Runtime Verification\u201418th International Conference, RV 2018, Limassol, Cyprus, November 10\u201313, 2018, Proceedings, volume 11237 of Lecture Notes in Computer Science, pp. 113\u2013137. Springer (2018)","DOI":"10.1007\/978-3-030-03769-7_8"},{"key":"1143_CR12","doi-asserted-by":"crossref","unstructured":"Barnett, M., Chang, B.Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: A modular reusable verifier for object-oriented programs. In: FMCO 2005, pp. 364\u2013387. Springer (2005)","DOI":"10.1007\/11804192_17"},{"key":"1143_CR13","unstructured":"Barros, G., Gallagher, P.: EIP-1822: universal Upgradeable Proxy Standard (UUPS). https:\/\/eips.ethereum.org\/EIPS\/eip-1822"},{"key":"1143_CR14","doi-asserted-by":"crossref","unstructured":"Bernardo, B., Cauderlier, R., Hu, Z., Pesin, B., Tesson, J.: Mi-cho-coq, a framework for certifying tezos smart contracts. In: Formal Methods. FM 2019 International Workshops: Porto, Portugal, October 7\u201311, 2019, Revised Selected Papers, Part I 3, pp. 368\u2013379. Springer (2020)","DOI":"10.1007\/978-3-030-54994-7_28"},{"key":"1143_CR15","doi-asserted-by":"crossref","unstructured":"Biryukov, A., Khovratovich, D., Tikhomirov, S.: Findel: secure derivative contracts for ethereum. In: Financial Cryptography and Data Security\u2014FC 2017 International Workshops, pp. 453\u2013467. FC (2017)","DOI":"10.1007\/978-3-319-70278-0_28"},{"key":"1143_CR16","doi-asserted-by":"crossref","unstructured":"Br\u00fcnnler, K., Flumini, D., Studer, T.: A logic of blockchain updates. In: Logical Foundations of Computer Science: International Symposium, LFCS 2018, Deerfield Beach, FL, USA, January 8\u201311, 2018, Proceedings, pp. 107\u2013119. Springer (2017)","DOI":"10.1007\/978-3-319-72056-2_7"},{"key":"1143_CR17","unstructured":"Ca\u00f1ada, A.C., Kobayashi, F., Fubuloubu, Williams, A.: Erc-3156: Flash loans. Ethereum Improvement Proposals, 3156, 2020. https:\/\/eips.ethereum.org\/EIPS\/eip-3156"},{"key":"1143_CR18","doi-asserted-by":"crossref","unstructured":"Dickerson, T., Gazzillo, P., Herlihy, M., Saraph, V., Koskinen, E.: Proof-carrying smart contracts. In: Financial Cryptography Workshops (2018)","DOI":"10.1007\/978-3-662-58820-8_22"},{"key":"1143_CR19","doi-asserted-by":"publisher","first-page":"110598","DOI":"10.1016\/j.jss.2020.110598","volume":"167","author":"J Dihego","year":"2020","unstructured":"Dihego, J., Sampaio, A., Oliveira, M.: A refinement checking based strategy for component-based systems evolution. J. Syst. Softw. 167, 110598 (2020)","journal-title":"J. Syst. Softw."},{"key":"1143_CR20","doi-asserted-by":"crossref","unstructured":"Durieux, T., Ferreira, J.F., Abreu, R., Cruz, P.: Empirical review of automated analysis tools on 47,587 ethereum smart contracts. In: Proceedings of the ACM\/IEEE 42nd International Conference on Software Engineering, ICSE\u201920, pp. 530\u2013541. Association for Computing Machinery, New York (2020)","DOI":"10.1145\/3377811.3380364"},{"issue":"3","key":"1143_CR21","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1109\/5.558710","volume":"85","author":"S Edwards","year":"1997","unstructured":"Edwards, S., Lavagno, L., Lee, E.A., Sangiovanni-Vincentelli, A.: Design of embedded systems: formal models, validation, and synthesis. Proc. IEEE 85(3), 366\u2013390 (1997)","journal-title":"Proc. IEEE"},{"key":"1143_CR22","unstructured":"Entriken, W., Shirley, D., Evans, J., Sachs, N.: Erc-721: non-fungible token standard. Ethereum Improvement Proposals, 721, (2018). https:\/\/eips.ethereum.org\/EIPS\/eip-721"},{"key":"1143_CR23","unstructured":"Ethereum White Paper. https:\/\/github.com\/ethereum\/wiki\/wiki\/White-Paper"},{"key":"1143_CR24","unstructured":"Ethereum Yellow Paper. https:\/\/ethereum.github.io\/yellowpaper\/paper.pdf"},{"key":"1143_CR25","doi-asserted-by":"crossref","unstructured":"Galimullin, R., \u00c5gotnes, T.: Coalition logic for specification and verification of smart contract upgrades. In: PRIMA 2022: Principles and Practice of Multi-Agent Systems: 24th International Conference, Valencia, Spain, November 16\u201318, 2022, Proceedings, pp. 563\u2013572. Springer (2022)","DOI":"10.1007\/978-3-031-21203-1_34"},{"key":"1143_CR26","unstructured":"Goodman, L.M.: Tezos-a self-amending crypto-ledger white paper (2014). https:\/\/www.tezos.com\/static\/papers\/whitepaper.pdf"},{"key":"1143_CR27","unstructured":"Grishchenko, I., Maffei, M., Schneidewind, C.: Ethertrust: sound static analysis of ethereum bytecode. Technische Universit\u00e4t Wien, Tech. Rep (2018)"},{"key":"1143_CR28","doi-asserted-by":"crossref","unstructured":"Groce, A., Feist, J., Grieco, G., Colburn, M.: What are the actual flaws in important smart contracts (and how can we find them)? In: Bonneau, J., Heninger, N. (eds.) Financial Cryptography and Data Security, pp. 634\u2013653. Springer, Cham (2020)","DOI":"10.1007\/978-3-030-51280-4_34"},{"key":"1143_CR29","doi-asserted-by":"crossref","unstructured":"Hahn, A., Singh, R., Liu, C.C., Chen, S.: Smart contract-based campus demonstration of decentralized transactive energy auctions. In: 2017 IEEE Power & Energy Society Innovative Smart Grid Technologies Conference, pp. 1\u20135. IEEE (2017)","DOI":"10.1109\/ISGT.2017.8086092"},{"key":"1143_CR30","doi-asserted-by":"crossref","unstructured":"Hajdu, \u00c1., Jovanovi\u0107, D.: SMT-friendly formalization of the solidity memory model. In: ESOP 2020, pp. 224\u2013250. Springer (2020)","DOI":"10.1007\/978-3-030-44914-8_9"},{"key":"1143_CR31","doi-asserted-by":"crossref","unstructured":"Hajdu, \u00c1., Jovanovi\u0107, D.: solc-verify: a modular verifier for solidity smart contracts. In: VSTTE, pp. 161\u2013179. Springer (2020)","DOI":"10.1007\/978-3-030-41600-3_11"},{"key":"1143_CR32","unstructured":"Heineman, G.T., Councill, W.T.: Component-based software engineering. In: Putting the pieces together, Addison-Westley, vol. 5, p. 1 (2001)"},{"key":"1143_CR33","doi-asserted-by":"crossref","unstructured":"Herlihy, M., Moir, M.: Blockchains and the logic of accountability: keynote address. In: Proceedings of the 31st Annual ACM\/IEEE Symposium on Logic in Computer Science, pp. 27\u201330 (2016)","DOI":"10.1145\/2933575.2934579"},{"key":"1143_CR34","doi-asserted-by":"crossref","unstructured":"Hildenbrandt, E., Saxena, M., Rodrigues, N., Zhu, X., Daian, P., Guth, D., Moore, B., Park, D., Zhang, Y., Stefanescu, A., et\u00a0al.: Kevm: a complete formal semantics of the ethereum virtual machine. In:  CSF 2018, pp. 204\u2013217. IEEE (2018)","DOI":"10.1109\/CSF.2018.00022"},{"issue":"2","key":"1143_CR35","doi-asserted-by":"publisher","first-page":"100179","DOI":"10.1016\/j.patter.2020.100179","volume":"2","author":"B Hu","year":"2021","unstructured":"Hu, B., Zhang, Z., Liu, J., Liu, Y., Yin, J., Lu, R., Lin, X.: A comprehensive survey on smart contract construction and execution: paradigms, tools, and systems. Patterns 2(2), 100179 (2021)","journal-title":"Patterns"},{"issue":"1","key":"1143_CR36","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1109\/TSE.1985.231535","volume":"11","author":"RA Kemmerer","year":"1985","unstructured":"Kemmerer, R.A.: Testing formal specifications to detect design errors. IEEE Trans. Softw. Eng. 11(1), 32\u201343 (1985)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"1143_CR37","first-page":"175","volume-title":"JML: A Notation for Detailed Design","author":"GT Leavens","year":"1999","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: A Notation for Detailed Design, pp. 175\u2013188. Springer, Boston (1999)"},{"key":"1143_CR38","doi-asserted-by":"crossref","unstructured":"Lee, J., Nikitin, K., Setty, S.: Replicated state machines without replicated execution. In: IEEE (2020)","DOI":"10.1109\/SP40000.2020.00068"},{"issue":"131","key":"1143_CR39","first-page":"9","volume":"178","author":"KRM Leino","year":"2008","unstructured":"Leino, K.R.M.: This is boogie 2. manuscript KRML 178(131), 9 (2008)","journal-title":"manuscript KRML"},{"key":"1143_CR40","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, pp. 348\u2013370. Springer, Berlin (2010)"},{"issue":"6","key":"1143_CR41","doi-asserted-by":"publisher","first-page":"1811","DOI":"10.1145\/197320.197383","volume":"16","author":"BH Liskov","year":"1994","unstructured":"Liskov, B.H., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16(6), 1811\u20131841 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"1143_CR42","doi-asserted-by":"crossref","unstructured":"Liu, C., Liu, H., Cao, Z., Chen, Z., Chen, B., Roscoe, B.: Reguard: finding reentrancy bugs in smart contracts. In: ICSE 2018, pp. 65\u201368. ACM (2018)","DOI":"10.1145\/3183440.3183495"},{"key":"1143_CR43","doi-asserted-by":"crossref","unstructured":"Liu, S.: Verifying consistency and validity of formal specifications by testing. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM\u201999\u2014Formal Methods, pp. 896\u2013914. Springer, Berlin (1999)","DOI":"10.1007\/3-540-48119-2_49"},{"key":"1143_CR44","unstructured":"Lorentz Documentation: https:\/\/wiki.tezos.com\/build\/smart-contracts\/morley-framework\/lorentz"},{"key":"1143_CR45","doi-asserted-by":"crossref","unstructured":"Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: CCS 2016, pp. 254\u2013269. ACM (2016)","DOI":"10.1145\/2976749.2978309"},{"issue":"3","key":"1143_CR46","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1109\/TC.2017.2647955","volume":"67","author":"P Maene","year":"2018","unstructured":"Maene, P., G\u00f6tzfried, J., de Clercq, R., M\u00fcller, T., Freiling, F., Verbauwhede, I.: Hardware-based trusted computing architectures for isolation and attestation. IEEE Trans. Comput. 67(3), 361\u2013374 (2018)","journal-title":"IEEE Trans. Comput."},{"key":"1143_CR47","doi-asserted-by":"crossref","unstructured":"McCorry, P., Shahandashti, S.F., Hao, F.: A smart contract for boardroom voting with maximum voter privacy. In: Kiayias, A. (eds.) Financial Cryptography and Data Security. FC 2017. Lecture Notes in Computer Science, volume 10322, pp. 357\u2013375 (2017)","DOI":"10.1007\/978-3-319-70972-7_20"},{"issue":"10","key":"1143_CR48","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B Meyer","year":"1992","unstructured":"Meyer, B.: Applying \u201cdesign by contract\u2019\u2019. Computer 25(10), 40\u201351 (1992)","journal-title":"Computer"},{"key":"1143_CR49","volume-title":"Object-Oriented Software Construction","author":"B Meyer","year":"1988","unstructured":"Meyer, B.: Object-Oriented Software Construction, 1st edn. Prentice-Hall Inc, Hoboken (1988)","edition":"1"},{"key":"1143_CR50","volume-title":"Programming from Specifications","author":"C Morgan","year":"1994","unstructured":"Morgan, C.: Programming from Specifications, 2nd edn. Prentice Hall International (UK) Ltd., Hoboken (1994)","edition":"2"},{"key":"1143_CR51","doi-asserted-by":"crossref","unstructured":"Mossberg, M., Manzano, F., Hennenfent, E., Groce, A., Grieco, G., Feist, J., Brunson, T., Dinaburg, A.: Manticore: a user-friendly symbolic execution framework for binaries and smart contracts. In: 2019 34th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 1186\u20131189. IEEE (2019)","DOI":"10.1109\/ASE.2019.00133"},{"key":"1143_CR52","unstructured":"Mudge, N.: EIP-2535: Diamonds, Multi-Facet Proxy. https:\/\/eips.ethereum.org\/EIPS\/eip-2535"},{"key":"1143_CR53","doi-asserted-by":"crossref","unstructured":"Nguyen, T.D., Pham, L.H., Sun, J.: Sguard: towards fixing vulnerable smart contracts automatically. In: 2021 IEEE Symposium on Security and Privacy (SP), pp. 1215\u20131229 (2021)","DOI":"10.1109\/SP40001.2021.00057"},{"issue":"2","key":"1143_CR54","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2794381","volume":"48","author":"CB Nielsen","year":"2015","unstructured":"Nielsen, C.B., Larsen, P.G., Fitzgerald, J., Woodcock, J., Peleska, J.: Systems of systems engineering: basic concepts, model-based techniques, and research directions. ACM Comput. Surv. 48(2), 1\u201341 (2015)","journal-title":"ACM Comput. Surv."},{"key":"1143_CR55","doi-asserted-by":"crossref","unstructured":"Notheisen, B., G\u00f6dde, M., Weinhardt, C.: Trading stocks on blocks\u2014engineering decentralized markets. In: Hevner, A. (eds.) Designing the Digital Transformation. DESRIST 2017. Lecture Notes in Computer Science (2017)","DOI":"10.1007\/978-3-319-59144-5_34"},{"key":"1143_CR56","unstructured":"Palladino, S.: EIP-1967: Standard Proxy Storage Slots. https:\/\/eips.ethereum.org\/EIPS\/eip-1967"},{"issue":"11","key":"1143_CR57","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1109\/MC.2007.400","volume":"40","author":"MP Papazoglou","year":"2007","unstructured":"Papazoglou, M.P., Traverso, P., Dustdar, S., Leymann, F.: Service-oriented computing: state of the art and research challenges. Computer 40(11), 38\u201345 (2007)","journal-title":"Computer"},{"key":"1143_CR58","doi-asserted-by":"crossref","unstructured":"Permenev, A., Dimitrov, D., Tsankov, P., Drachsler-Cohen, D., Vechev, M.: Verx: safety verification of smart contracts. In: S &P 2020, pp. 18\u201320 (2020)","DOI":"10.1109\/SP40000.2020.00024"},{"key":"1143_CR59","unstructured":"Radomski, W., Cooke, A., Castonguay, P., Therien, J., Binet, E., Sandford, R.: EIP-1155: Token Standard. https:\/\/eips.ethereum.org\/EIPS\/eip-1155"},{"key":"1143_CR60","unstructured":"Rodler, M., Li, W., Karame, G.O., Davi, L.: Evmpatch: timely and automated patching of ethereum smart contracts. In: 30th USENIX Security Symposium (USENIX Security 21), pp. 1289\u20131306. USENIX Association (2021)"},{"key":"1143_CR61","doi-asserted-by":"crossref","unstructured":"Shorish, J.: Blockchain state machine representation (2018)","DOI":"10.31235\/osf.io\/eusxg"},{"key":"1143_CR62","unstructured":"Siegel, D.: Understanding the DAO attack. https:\/\/www.coindesk.com\/understanding-dao-hack-journalists. Accessed 25 Sept (2023)"},{"key":"1143_CR63","unstructured":"Solidity Compiler: https:\/\/github.com\/ethereum\/solidity"},{"issue":"4","key":"1143_CR64","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1109\/54.936247","volume":"18","author":"S Tasiran","year":"2001","unstructured":"Tasiran, S., Keutzer, K.: Coverage metrics for functional validation of hardware designs. IEEE Des. Test Comput. 18(4), 36\u201345 (2001)","journal-title":"IEEE Des. Test Comput."},{"key":"1143_CR65","unstructured":"OpenZeppelin Team: Proxy Upgrade Pattern. https:\/\/docs.openzeppelin.com\/upgrades-plugins\/1.x\/proxies"},{"key":"1143_CR66","doi-asserted-by":"crossref","unstructured":"Tikhomirov, S., Voskresenskaya, E., Ivanitskiy, I., Takhaviev, R., Marchenko, E., Alexandrov, Y.: Smartcheck: static analysis of ethereum smart contracts. In: WETSEB 2018, pp. 9\u201316. IEEE (2018)","DOI":"10.1145\/3194113.3194115"},{"issue":"7","key":"1143_CR67","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3464421","volume":"54","author":"P Tolmach","year":"2021","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), 1\u201338 (2021)","journal-title":"ACM Comput. Surv."},{"key":"1143_CR68","unstructured":"Torres, C.F., Jonker, H., State, R.: Elysium: automagically healing vulnerable smart contracts using context-aware patching. In: CoRR, abs\/2108.10071 (2021)"},{"key":"1143_CR69","doi-asserted-by":"crossref","unstructured":"Tsankov, P., Dan, A., Drachsler-Cohen, D., Gervais, A., Buenzli, F., Vechev, M.: Securify: practical security analysis of smart contracts. In: CCS 2018, pp. 67\u201382. ACM (2018)","DOI":"10.1145\/3243734.3243780"},{"key":"1143_CR70","unstructured":"Vogelsteller, F., Buterin, V.: EIP-20: token standard. https:\/\/eips.ethereum.org\/EIPS\/eip-20"},{"key":"1143_CR71","unstructured":"Vollmer, J.: The biggest hacker whodunnit of the summer. https:\/\/www.vice.com\/en\/article\/pgkzqm\/the-biggest-hacker-whodunnit-of-the-summer. Accessed 25 Sept 2023"},{"key":"1143_CR72","doi-asserted-by":"crossref","unstructured":"Wang, D., Wu, S., Lin, Z., Wu, L., Yuan, X., Zhou, Y., Wang, H., Ren, K.: Towards a first step to understand flash loan and its applications in defi ecosystem. In: Proceedings of the Ninth International Workshop on Security in Blockchain and Cloud Computing, pp. 23\u201328 (2021)","DOI":"10.1145\/3457977.3460301"},{"key":"1143_CR73","doi-asserted-by":"crossref","unstructured":"Wang, Y., Lahiri, S.K., Chen, S., Pan, R., Dillig, I., Born, C., Naseer, I., Ferles, K.: Formal verification of workflow policies for smart contracts in azure blockchain. In: VSTTE, pp. 87\u2013106 (2020)","DOI":"10.1007\/978-3-030-41600-3_7"},{"key":"1143_CR74","unstructured":"Wood, G.: Ethereum: a secure decentralised generalised transaction ledger (2014)"},{"key":"1143_CR75","doi-asserted-by":"crossref","unstructured":"W\u00fcst, K., Matetic, S., Egli, S., Kostiainen, K., Capkun, S.: Ace: asynchronous and concurrent execution of complex smart contracts. In: Proceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security, CCS\u201920, pp 587\u2013600 (2020)","DOI":"10.1145\/3372297.3417243"},{"key":"1143_CR76","volume-title":"Enabling the Internet of Value. Future of Business and Finance","author":"J Xu","year":"2022","unstructured":"Xu, J., Vadgama, N.: From banks to DeFi: the evolution of the lending market. In: Vadgama, N., Xu, J., Tasca, P. (eds.) Enabling the Internet of Value. Future of Business and Finance. Springer, Cham (2022)"},{"key":"1143_CR77","doi-asserted-by":"crossref","unstructured":"Yermack, D.: Corporate governance and blockchains. In: Review of Finance, pp. 7\u201331 (2017)","DOI":"10.1093\/rof\/rfw074"},{"issue":"4","key":"1143_CR78","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3402450","volume":"29","author":"XL Yu","year":"2020","unstructured":"Yu, X.L., Al-Bataineh, O., Lo, D., Roychoudhury, A.: Smart contract repair. ACM Trans. Softw. Eng. Methodol. 29(4), 1\u201332 (2020)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"1143_CR79","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1016\/j.future.2019.12.019","volume":"105","author":"Z Zheng","year":"2020","unstructured":"Zheng, Z., Xie, S., Dai, H.-N., Chen, W., Chen, X., Weng, J., Imran, M.: An overview on smart contracts: Challenges, advances and platforms. Future Gener. Comput. Syst. 105, 475\u2013491 (2020). https:\/\/doi.org\/10.1016\/j.future.2019.12.019","journal-title":"Future Gener. Comput. Syst."}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-023-01143-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-023-01143-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-023-01143-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,20]],"date-time":"2024-07-20T04:14:53Z","timestamp":1721448893000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-023-01143-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,25]]},"references-count":79,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2024,6]]}},"alternative-id":["1143"],"URL":"https:\/\/doi.org\/10.1007\/s10270-023-01143-z","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,25]]},"assertion":[{"value":"28 February 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"10 October 2023","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 December 2023","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 January 2024","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}