{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,14]],"date-time":"2025-04-14T14:29:24Z","timestamp":1744640964567,"version":"3.40.3"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030674441"},{"type":"electronic","value":"9783030674458"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/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":"http:\/\/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-030-67445-8_14","type":"book-chapter","created":{"date-parts":[[2021,2,1]],"date-time":"2021-02-01T04:28:24Z","timestamp":1612153704000},"page":"323-348","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Model-Based Static and Runtime Verification for Ethereum Smart Contracts"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2165-3698","authenticated-orcid":false,"given":"Shaun","family":"Azzopardi","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2844-5728","authenticated-orcid":false,"given":"Christian","family":"Colombo","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0743-6272","authenticated-orcid":false,"given":"Gordon","family":"Pace","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,2,2]]},"reference":[{"key":"14_CR1","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., et al.: Verification of smart contract business logic - exploiting a Java source code verifier. In: Hojjat, H., Massink, M. (eds.) Fundamentals of Software Engineering - 8th International Conference, FSEN 2019, Tehran, Iran, May 1\u20133, 2019, Revised Selected Papers. Lecture Notes in Computer Science, vol. 11761, pp. 228\u2013243. Springer, Heidelberg (2019). https:\/\/doi.org\/10.1007\/978-3-030-31517-7_16","DOI":"10.1007\/978-3-030-31517-7_16"},{"key":"14_CR2","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Pace, G.J., Schneider, G.: A unified approach for static and runtime verification: framework and applications. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation - 5th International Symposium, ISoLA 2012, Heraklion, Crete, Greece, Proceedings, Part I. LNCS, vol. 7609, pp. 312\u2013326. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34026-0_24","DOI":"10.1007\/978-3-642-34026-0_24"},{"key":"14_CR3","doi-asserted-by":"publisher","unstructured":"Albert, E., Correas, J., Gordillo, P., Rom\u00e1n-D\u00edez, G., Rubio, A.: SAFEVM: a safety verifier for Ethereum smart contracts. In: Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2019, pp. 386\u2013389. Association for Computing Machinery, New York (2019). https:\/\/doi.org\/10.1145\/3293882.3338999","DOI":"10.1145\/3293882.3338999"},{"key":"14_CR4","doi-asserted-by":"publisher","unstructured":"Angelo, M.D., Salzer, G.: A survey of tools for analyzing Ethereum smart contracts. In: IEEE International Conference on Decentralized Applications and Infrastructures, DAPPCON 2019, Newark, CA, USA, April 4\u20139, 2019, pp. 69\u201378. IEEE (2019). https:\/\/doi.org\/10.1109\/DAPPCON.2019.00018","DOI":"10.1109\/DAPPCON.2019.00018"},{"key":"14_CR5","doi-asserted-by":"publisher","unstructured":"Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on Ethereum smart contracts SoK. In: Proceedings of the 6th International Conference on Principles of Security and Trust, vol. 10204, pp. 164\u2013186. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54455-6_8","DOI":"10.1007\/978-3-662-54455-6_8"},{"key":"14_CR6","unstructured":"Azzopardi, S., Colombo, C., Pace, G.: A technique for automata-based verification with residual reasoning. Tech. rep. CS-2019-02, Department of Computer Science, University of Malta (2019). https:\/\/www.um.edu.mt\/ict\/cs\/ourresearch\/technicalreports"},{"key":"14_CR7","doi-asserted-by":"publisher","unstructured":"Azzopardi, S., Colombo, C., Pace, G.J.: A model-based approach to combining static and dynamic verification techniques. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10\u201314, 2016, Proceedings, Part I. Lecture Notes in Computer Science, vol. 9952, pp. 416\u2013430. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47166-2_29","DOI":"10.1007\/978-3-319-47166-2_29"},{"key":"14_CR8","doi-asserted-by":"publisher","unstructured":"Azzopardi, S., Colombo, C., Pace, G.J.: Control-flow residual analysis for symbolic automata. In: Francalanza, A., Pace, G.J. (eds.) Proceedings Second International Workshop on Pre- and Post-Deployment Verification Techniques, Torino, Italy, 19 September 2017. Electronic Proceedings in Theoretical Computer Science, vol. 254, pp. 29\u201343. Open Publishing Association (2017). https:\/\/doi.org\/10.4204\/EPTCS.254.3","DOI":"10.4204\/EPTCS.254.3"},{"key":"14_CR9","unstructured":"Azzopardi, S., Colombo, C., Pace, G.J.: A technique for automata-based verification with residual reasoning. In: Model-Driven Engineering and Software Development - 8th International Conference, MODELSWARD 2020, Valletta, Malta, February 25\u201327, 2020 (2020)"},{"key":"14_CR10","unstructured":"Azzopardi, S., Colombo, C., Pace, G.J.: CLarva: model-based residual verification of java programs. In: Model-Driven Engineering and Software Development - 8th International Conference, MODELSWARD 2020, Valletta, Malta, February 25\u201327, 2020 (2020)"},{"key":"14_CR11","doi-asserted-by":"publisher","unstructured":"Azzopardi, S., Ellul, J., Pace, G.J.: Monitoring smart contracts: contractLarva and open challenges beyond. In: Colombo, C., Leucker, M. (eds.) Runtime Verification, pp. 113\u2013137. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03769-7_8","DOI":"10.1007\/978-3-030-03769-7_8"},{"key":"14_CR12","doi-asserted-by":"publisher","unstructured":"Azzopardi, S., Pace, G.J., Schapachnik, F.: On observing contracts: deontic contracts meet smart contracts. In: Palmirani, M. (ed.) Legal Knowledge and Information Systems - JURIX 2018: The Thirty-first Annual Conference, Groningen, The Netherlands, 12\u201314 December 2018. Frontiers in Artificial Intelligence and Applications, vol. 313, pp. 21\u201330. IOS Press (2018). https:\/\/doi.org\/10.3233\/978-1-61499-935-5-21","DOI":"10.3233\/978-1-61499-935-5-21"},{"key":"14_CR13","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: version 2.0. In: Gupta, A., Kroening, D. (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, Edinburgh, UK (2010)"},{"key":"14_CR14","doi-asserted-by":"publisher","unstructured":"Beyer, D., Henzinger, T.A., Keremoglu, M.E., Wendler, P.: Conditional model checking: a technique to pass information between verifiers. In: Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering, FSE 2012, pp. 57:1\u201357:11. ACM, New York (2012). https:\/\/doi.org\/10.1145\/2393596.2393664","DOI":"10.1145\/2393596.2393664"},{"key":"14_CR15","doi-asserted-by":"publisher","unstructured":"Beyer, D., Jakobs, M.C., Lemberger, T., Wehrheim, H.: Reducer-based construction of conditional verifiers. In: Proceedings of the 40th International Conference on Software Engineering, ICSE 2018, pp. 1182\u20131193. ACM, New York (2018). https:\/\/doi.org\/10.1145\/3180155.3180259","DOI":"10.1145\/3180155.3180259"},{"key":"14_CR16","doi-asserted-by":"publisher","unstructured":"Bodden, E., Lam, P.: Clara: partially evaluating runtime monitors at compile time. In: Barringer, H., et al. (eds.) Runtime Verification. RV 2010. Lecture Notes in Computer Science, vol. 6418. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16612-9_8","DOI":"10.1007\/978-3-642-16612-9_8"},{"key":"14_CR17","doi-asserted-by":"publisher","unstructured":"Dwyer, M.B., Purandare, R.: Residual dynamic typestate analysis exploiting static analysis: results to reformulate and reduce the cost of dynamic analysis. In: Proceedings of the Twenty-Second IEEE\/ACM International Conference on Automated Software Engineering, ASE 2007, pp. 124\u2013133. ACM, New York (2007). https:\/\/doi.org\/10.1145\/1321631.1321651","DOI":"10.1145\/1321631.1321651"},{"key":"14_CR18","doi-asserted-by":"publisher","unstructured":"Dwyer, M.B., Purandare, R.: Residual checking of safety properties. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) Model Checking Software. SPIN 2008. Lecture Notes in Computer Science, vol. 5156. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-85114-1_1","DOI":"10.1007\/978-3-540-85114-1_1"},{"key":"14_CR19","doi-asserted-by":"publisher","unstructured":"Ellul, J., Pace, G.J.: Runtime verification of Ethereum smart contracts. In: 14th European Dependable Computing Conference, EDCC 2018, Ia\u015fi, Romania, September 10\u201314, 2018, pp. 158\u2013163. IEEE Computer Society (2018). https:\/\/doi.org\/10.1109\/EDCC.2018.00036","DOI":"10.1109\/EDCC.2018.00036"},{"key":"14_CR20","doi-asserted-by":"publisher","unstructured":"Falcone, Y., Krsti\u0107, S., Reger, G., Traytel, D.: A taxonomy for classifying runtime verification tools. In: Colombo, C., Leucker, M. (eds.) Runtime Verification. RV 2018. Lecture Notes in Computer Science, vol. 11237. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03769-7_14","DOI":"10.1007\/978-3-030-03769-7_14"},{"key":"14_CR21","doi-asserted-by":"publisher","unstructured":"Hildenbrandt, E., et al.: KEVM: a complete formal semantics of the Ethereum virtual machine. In: 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9\u201312, 2018, pp. 204\u2013217. IEEE Computer Society (2018). https:\/\/doi.org\/10.1109\/CSF.2018.00022","DOI":"10.1109\/CSF.2018.00022"},{"key":"14_CR22","doi-asserted-by":"publisher","unstructured":"Li, A., Choi, J.A., Long, F.: Securing smart contract with runtime validation. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2020, pp. 438\u2013453. Association for Computing Machinery, New York (2020). https:\/\/doi.org\/10.1145\/3385412.3385982","DOI":"10.1145\/3385412.3385982"},{"key":"14_CR23","doi-asserted-by":"publisher","unstructured":"Mavridou, A., Laszka, A.: Designing secure Ethereum smart contracts: a finite state machine based approach. In: Meiklejohn, S., Sako, K. (eds.) Financial Cryptography and Data Security - 22nd International Conference, FC 2018, Nieuwpoort, Cura\u00e7ao, February 26\u2013March 2, 2018, Revised Selected Papers. Lecture Notes in Computer Science, vol. 10957, pp. 523\u2013540. Springer, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-662-58387-6_28","DOI":"10.1007\/978-3-662-58387-6_28"},{"key":"14_CR24","doi-asserted-by":"publisher","unstructured":"Mavridou, A., Laszka, A., Stachtiari, E., Dubey, A.: VeriSolid: correct-by-design smart contracts for Ethereum. In: Goldberg, I., Moore, T. (eds.) Financial Cryptography and Data Security, pp. 446\u2013465. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-32101-727","DOI":"10.1007\/978-3-030-32101-727"},{"key":"14_CR25","doi-asserted-by":"publisher","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2008. Lecture Notes in Computer Science, vol. 4963. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"14_CR26","doi-asserted-by":"publisher","first-page":"101129","DOI":"10.1016\/j.pmcj.2020.101129","volume":"63","author":"T Osterland","year":"2020","unstructured":"Osterland, T., Rose, T.: Model checking smart contracts for Ethereum. Pervasive Mob. Comput. 63, 101129 (2020). https:\/\/doi.org\/10.1016\/j.pmcj.2020.101129","journal-title":"Pervasive Mob. Comput."},{"key":"14_CR27","doi-asserted-by":"publisher","unstructured":"Park, D., Zhang, Y., Saxena, M., Daian, P., Ro\u015fu, G.: A formal verification tool for Ethereum VM bytecode. In: Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/FSE 2018, pp. 912\u2013915. Association for Computing Machinery, New York (2018). https:\/\/doi.org\/10.1145\/3236024.3264591","DOI":"10.1145\/3236024.3264591"},{"key":"14_CR28","doi-asserted-by":"crossref","unstructured":"Permenev, A., Dimitrov, D., Tsankov, P., Drachsler-Cohen, D., Vechev, M.: VerX: safety verification of smart contracts. In: 2020 IEEE Symposium on Security and Privacy (SP), pp. 414\u2013430. IEEE Computer Society, Los Alamitos (May 2020)","DOI":"10.1109\/SP40000.2020.00024"},{"key":"14_CR29","unstructured":"Tran, A.B., Lu, Q., Weber, I.: Lorikeet: a model-driven engineering tool for blockchain-based business process execution and asset management. In: van der Aalst, W.M.P., et al. (eds.) Proceedings of the Dissertation Award, Demonstration, and Industrial Track at BPM 2018 Co-located with 16th International Conference on Business Process Management (BPM 2018), Sydney, Australia, September 9\u201314, 2018. CEUR Workshop Proceedings, vol. 2196, pp. 56\u201360. CEUR-WS.org (2018)"},{"key":"14_CR30","first-page":"1","volume":"151","author":"G Wood","year":"2014","unstructured":"Wood, G.: Ethereum: a secure decentralised generalised transaction ledger. Ethereum Proj. Yellow Pap. 151, 1\u201332 (2014)","journal-title":"Ethereum Proj. Yellow Pap."},{"key":"14_CR31","doi-asserted-by":"publisher","unstructured":"Xu, X., Weber, I., Staples, M.: Model-driven engineering for blockchain applications. In: Architecture for Blockchain Applications. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-03035-3_8","DOI":"10.1007\/978-3-030-03035-3_8"},{"key":"14_CR32","doi-asserted-by":"publisher","unstructured":"Zhang, Y., Ma, S., Li, J., Li, K., Nepal, S., Gu, D.: Smartshield: automatic smart contract protection made easy. In: 2020 IEEE 27th International Conference on Software Analysis, Evolution and Reengineering (SANER), pp. 23\u201334 (February 2020). https:\/\/doi.org\/10.1109\/SANER48275.2020.9054825","DOI":"10.1109\/SANER48275.2020.9054825"}],"container-title":["Communications in Computer and Information Science","Model-Driven Engineering and Software Development"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-67445-8_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,2,1]],"date-time":"2021-02-01T04:34:01Z","timestamp":1612154041000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-67445-8_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030674441","9783030674458"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-67445-8_14","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"2 February 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"MODELSWARD","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Model-Driven Engineering and Software Development","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Valletta","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Malta","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 February 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 February 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"modelsward2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.modelsward.org\/?y=2020","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"PRIMORIS","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"66","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"15","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"23% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}