{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T22:48:37Z","timestamp":1767998917507,"version":"3.49.0"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031150074","type":"print"},{"value":"9783031150081","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"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":[[2022]]},"DOI":"10.1007\/978-3-031-15008-1_5","type":"book-chapter","created":{"date-parts":[[2022,9,4]],"date-time":"2022-09-04T23:02:47Z","timestamp":1662332567000},"page":"50-66","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Deductive Verification of\u00a0Smart Contracts with\u00a0Dafny"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4317-5025","authenticated-orcid":false,"given":"Franck","family":"Cassez","sequence":"first","affiliation":[]},{"given":"Joanne","family":"Fuller","sequence":"additional","affiliation":[]},{"given":"Horacio Mijail Ant\u00f3n","family":"Quiles","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,9,5]]},"reference":[{"key":"5_CR1","series-title":"Lecture Notes in Computer Science","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.) ISoLA 2020. LNCS, vol. 12478, pp. 9\u201324. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61467-6_2"},{"key":"5_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/978-3-030-03427-6_28","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice","author":"L Alt","year":"2018","unstructured":"Alt, L., Reitwiessner, C.: SMT-based verification of solidity smart contracts. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11247, pp. 376\u2013388. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03427-6_28"},{"key":"5_CR3","doi-asserted-by":"publisher","unstructured":"Amani, S., B\u00e9gel, M., Bortin, M., Staples, M.: Towards verifying ethereum smart contract bytecode in Isabelle\/HOL. In: Andronick, J., Felty, A.P. (eds.) 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, pp. 66\u201377. ACM (2018). https:\/\/doi.org\/10.1145\/3167084","DOI":"10.1145\/3167084"},{"key":"5_CR4","doi-asserted-by":"publisher","unstructured":"Bhargavan, K., et al.: Formal verification of smart contracts. In: PLAS@CCS 2016. pp. 91\u201396. ACM (2016). https:\/\/doi.org\/10.1145\/2993600.2993611","DOI":"10.1145\/2993600.2993611"},{"key":"5_CR5","doi-asserted-by":"publisher","unstructured":"Br\u00e4m, C., Eilers, M., M\u00fcller, P., Sierra, R., Summers, A.J.: Rich specifications for ethereum smart contract verification. Proc. ACM Program. Lang.5(OOPSLA), 1\u201330 (2021). https:\/\/doi.org\/10.1145\/3485523","DOI":"10.1145\/3485523"},{"key":"5_CR6","doi-asserted-by":"publisher","unstructured":"Britten, D., Sj\u00f6berg, V., Reeves, S.: Using coq to enforce the checks-effects-interactions pattern in DeepSea smart contracts. In: Bernardo, B., Marmsoler, D. (eds.) 3rd International Workshop on Formal Methods for Blockchains, FMBC@CAV 2021. OASIcs, vol. 95, pp. 3:1\u20133:8. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/OASIcs.FMBC.2021.3","DOI":"10.4230\/OASIcs.FMBC.2021.3"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"445","DOI":"10.1007\/978-3-030-90870-6_24","volume-title":"Formal Methods","author":"F Cassez","year":"2021","unstructured":"Cassez, F.: Verification of the Incremental Merkle Tree Algorithm with Dafny. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 445\u2013462. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_24"},{"key":"5_CR8","unstructured":"Choo, L.: Crypto is crumbling, and DeFi hacks are getting worse. https:\/\/www.protocol.com\/fintech\/defi-hacks-web3"},{"key":"5_CR9","unstructured":"ConsenSys Diligence: Mythx, https:\/\/mythx.io\/"},{"key":"5_CR10","doi-asserted-by":"publisher","unstructured":"Dharanikota, S., Mukherjee, S., Bhardwaj, C., Rastogi, A., Lal, A.: Celestial: a smart contracts verification framework. In: Formal Methods in Computer Aided Design, FMCAD 2021, New Haven, CT, USA, pp. 133\u2013142. IEEE (2021). https:\/\/doi.org\/10.34727\/2021\/isbn.978-3-85448-046-4_22","DOI":"10.34727\/2021\/isbn.978-3-85448-046-4_22"},{"key":"5_CR11","unstructured":"Ethereum Foundation: Solidity documentation (2022). https:\/\/docs.soliditylang.org\/en\/v0.8.14\/"},{"key":"5_CR12","unstructured":"Fe Team: Fe: an emerging smart contract language for the Ethereum blockchain (2022). https:\/\/github.com\/ethereum\/fe"},{"key":"5_CR13","unstructured":"G\u00fc\u00e7l\u00fct\u00fcrk, O.G.: The DAO hack explained: unfortunate take-off of smart contracts (2018). https:\/\/ogucluturk.medium.com\/the-dao-hack-explained-unfortunate-take-off-of-smart-contracts-2bd8c8db3562"},{"key":"5_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/978-3-030-41600-3_11","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"\u00c1 Hajdu","year":"2020","unstructured":"Hajdu, \u00c1., Jovanovi\u0107, D.: solc-verify: a modular verifier for solidity smart contracts. In: Chakraborty, S., Navas, J.A. (eds.) VSTTE 2019. LNCS, vol. 12031, pp. 161\u2013179. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-41600-3_11"},{"key":"5_CR15","doi-asserted-by":"publisher","unstructured":"Hajdu, \u00c1., Jovanovic, D., Ciocarlie, G.F.: Formal specification and verification of Solidity contracts with events (short paper). In: Bernardo, B., Marmsoler, D. (eds.) 2nd Workshop on Formal Methods for Blockchains, FMBC@CAV 2020. OASIcs, vol. 84, pp. 2:1\u20132:9. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2020). https:\/\/doi.org\/10.4230\/OASIcs.FMBC.2020.2","DOI":"10.4230\/OASIcs.FMBC.2020.2"},{"key":"5_CR16","doi-asserted-by":"publisher","unstructured":"da Horta, L.P.A., Reis, J.S., de Sousa, S.M., Pereira, M.: A tool for proving Michelson smart contracts in WHY3. In: IEEE International Conference on Blockchain, Blockchain 2020. Rhodes, Greece, pp. 409\u2013414. IEEE (2020). https:\/\/doi.org\/10.1109\/Blockchain50366.2020.00059","DOI":"10.1109\/Blockchain50366.2020.00059"},{"issue":"6","key":"5_CR17","doi-asserted-by":"publisher","first-page":"94","DOI":"10.1109\/MS.2017.4121212","volume":"34","author":"KRM Leino","year":"2017","unstructured":"Leino, K.R.M.: Accessible software verification with Dafny. IEEE Softw. 34(6), 94\u201397 (2017). https:\/\/doi.org\/10.1109\/MS.2017.4121212","journal-title":"IEEE Softw."},{"key":"5_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1007\/978-3-030-61467-6_12","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Applications","author":"M Marescotti","year":"2020","unstructured":"Marescotti, M., Otoni, R., Alt, L., Eugster, P., Hyv\u00e4rinen, A.E.J., Sharygina, N.: Accurate smart contract verification through direct modelling. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12478, pp. 178\u2013194. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61467-6_12"},{"key":"5_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1007\/978-3-030-92124-8_23","volume-title":"Software Engineering and Formal Methods","author":"D Marmsoler","year":"2021","unstructured":"Marmsoler, D., Brucker, A.D.: A denotational semantics of\u00a0solidity in\u00a0isabelle\/HOL. In: Calinescu, R., P\u0103s\u0103reanu, C.S. (eds.) SEFM 2021. LNCS, vol. 13085, pp. 403\u2013422. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-92124-8_23"},{"key":"5_CR20","doi-asserted-by":"publisher","unstructured":"Neha\u00ef, Z., Bobot, F.: Deductive proof of industrial smart contracts using why3. In: Sekerinski, E., et al. (eds.) FM 2019. LNCS, vol. 12232, pp. 299\u2013311. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-54994-7_22","DOI":"10.1007\/978-3-030-54994-7_22"},{"key":"5_CR21","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"5_CR22","unstructured":"Park, D., Zhang, Y.: Formal verification of the incremental Merkle tree algorithm (2020). https:\/\/github.com\/runtimeverification\/verified-smart-contracts\/blob\/master\/deposit\/formal-incremental-merkle-tree-algorithm.pdf"},{"key":"5_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-030-53288-8_8","volume-title":"Computer Aided Verification","author":"D Park","year":"2020","unstructured":"Park, D., Zhang, Y., Rosu, G.: End-to-end formal verification of\u00a0ethereum 2.0 deposit smart contract. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 151\u2013164. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_8"},{"key":"5_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/978-3-642-35746-6_3","volume-title":"Tools for Practical Software Verification","author":"C Paulin-Mohring","year":"2012","unstructured":"Paulin-Mohring, C.: Introduction to the coq proof-assistant for practical software verification. In: Meyer, B., Nordio, M. (eds.) LASER 2011. LNCS, vol. 7682, pp. 45\u201395. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-35746-6_3"},{"key":"5_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-030-17601-3_1","volume-title":"Engineering Trustworthy Software Systems","author":"DJ Pearce","year":"2019","unstructured":"Pearce, D.J., Utting, M., Groves, L.: An introduction to software verification with whiley. In: Bowen, J.P., Liu, Z., Zhang, Z. (eds.) SETSS 2018. LNCS, vol. 11430, pp. 1\u201337. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17601-3_1"},{"key":"5_CR26","doi-asserted-by":"publisher","unstructured":"Schiffl, J., Ahrendt, W., Beckert, B., Bubel, R.: Formal analysis of smart contracts: applying the KeY system. In: Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Ulbrich, M. (eds.) Deductive Software Verification: Future Perspectives. LNCS, vol. 12345, pp. 204\u2013218. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-64354-6_8","DOI":"10.1007\/978-3-030-64354-6_8"},{"key":"5_CR27","unstructured":"Vyper Team: Documentation (2020). https:\/\/vyper.readthedocs.io\/en\/stable\/"},{"key":"5_CR28","doi-asserted-by":"publisher","unstructured":"Wesley, S., Christakis, M., Navas, J.A., Trefler, R., W\u00fcstholz, V., Gurfinkel, A.: Verifying solidity smart contracts via communication abstraction in SmartACE. In: Finkbeiner, B., Wies, T. (eds.) VMCAI 2022. LNCS, vol. 13182, pp. 425\u2013449. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-94583-1_21","DOI":"10.1007\/978-3-030-94583-1_21"},{"key":"5_CR29","unstructured":"Wood, D.: Ethereum: a secure decentralised generalised transaction ledger (2022). https:\/\/ethereum.github.io\/yellowpaper\/paper.pdf"},{"key":"5_CR30","doi-asserted-by":"crossref","unstructured":"W\u00fcstholz, V., Christakis, M.: Harvey: A Greybox Fuzzer for Smart Contracts, pp. 1398\u20131409. Association for Computing Machinery, New York (2020). https:\/\/doi.org\/10.1145\/3368089.3417064","DOI":"10.1145\/3368089.3417064"},{"key":"5_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-030-03592-1_13","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"J Zakrzewski","year":"2018","unstructured":"Zakrzewski, J.: Towards verification of Ethereum smart contracts: a formalization of core of solidity. In: Piskac, R., R\u00fcmmer, P. (eds.) VSTTE 2018. LNCS, vol. 11294, pp. 229\u2013247. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03592-1_13"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-15008-1_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,4]],"date-time":"2022-09-04T23:09:24Z","timestamp":1662332964000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-15008-1_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031150074","9783031150081"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-15008-1_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"5 September 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FMICS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Methods for Industrial Critical Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Warsaw","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Poland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 September 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 September 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fmics2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/fmics2022.fsa.win.tue.nl\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"22","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":"13","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":"59% - 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":"2.5","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":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}