{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:58:34Z","timestamp":1764403114501,"version":"3.40.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030908690"},{"type":"electronic","value":"9783030908706"}],"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-030-90870-6_24","type":"book-chapter","created":{"date-parts":[[2021,11,10]],"date-time":"2021-11-10T00:06:44Z","timestamp":1636502804000},"page":"445-462","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Verification of the Incremental Merkle Tree Algorithm with Dafny"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4317-5025","authenticated-orcid":false,"given":"Franck","family":"Cassez","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,11,10]]},"reference":[{"key":"24_CR1","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.) Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, Los Angeles, CA, USA, 8\u20139 January 2018, pp. 66\u201377. ACM (2018). https:\/\/doi.org\/10.1145\/3167084","DOI":"10.1145\/3167084"},{"key":"24_CR2","doi-asserted-by":"publisher","unstructured":"Andrici, C., Ciob\u00e2c\u0103, \u015e.: Verifying the DPLL algorithm in Dafny. In: Marin, M., Craciun, A. (eds.) Proceedings Third Symposium on Working Formal Methods, FROM 2019, EPTCS, Timi\u015foara, Romania, 3\u20135 September 2019, vol. 303, pp. 3\u201315 (2019). https:\/\/doi.org\/10.4204\/EPTCS.303.1","DOI":"10.4204\/EPTCS.303.1"},{"key":"24_CR3","unstructured":"Bugrara, S.: A review of the deposit contract (2020). https:\/\/github.com\/suhabe\/eth-deposit-contract-vyper-review\/blob\/master\/EthDepositContractVyperReview.pdf"},{"key":"24_CR4","unstructured":"Buterin, V.: Progressive Merkle tree. https:\/\/github.com\/ethereum\/research\/ blob\/master\/beacon_chain_impl\/progressive_merkle_tree.py"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-030-55089-9_4","volume-title":"Engineering Trustworthy Software Systems","author":"X Chen","year":"2020","unstructured":"Chen, X., Ro\u015fu, G.: $$\\mathbb{K}$$\u2014a semantic framework for programming languages and formal analysis. In: Bowen, J.P., Liu, Z., Zhang, Z. (eds.) SETSS 2019. LNCS, vol. 12154, pp. 122\u2013158. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-55089-9_4"},{"key":"24_CR6","unstructured":"ConsenSys Diligence: Mythx. https:\/\/mythx.io\/"},{"key":"24_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-319-21690-4_16","volume-title":"Computer Aided Verification","author":"S de Gouw","year":"2015","unstructured":"de Gouw, S., Rot, J., de Boer, F.S., Bubel, R., H\u00e4hnle, R.: OpenJDK\u2019s Java.utils.Collection.sort() is broken: the good, the bad and the worst case. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 273\u2013289. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_16"},{"key":"24_CR8","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":"24_CR9","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, Los Angeles, California, USA (Virtual Conference), 20\u201321 July 2020, 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":"24_CR10","doi-asserted-by":"publisher","unstructured":"Hawblitzel, C., et al.: IronFleet: proving practical distributed systems correct. In: Miller, E.L., Hand, S. (eds.) Proceedings of the 25th Symposium on Operating Systems Principles, SOSP 2015, Monterey, CA, USA, 4\u20137 October 2015, pp. 1\u201317. ACM (2015). https:\/\/doi.org\/10.1145\/2815400.2815428","DOI":"10.1145\/2815400.2815428"},{"key":"24_CR11","doi-asserted-by":"publisher","unstructured":"Klein, G., et al.: seL4: formal verification of an OS kernel. In: Matthews, J.N., Anderson, T.E. (eds.) Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, SOSP 2009, Big Sky, Montana, USA, 11\u201314 October 2009, pp. 207\u2013220. ACM (2009). https:\/\/doi.org\/10.1145\/1629575.1629596","DOI":"10.1145\/1629575.1629596"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-030-51054-1_18","volume-title":"Automated Reasoning","author":"P Lammich","year":"2020","unstructured":"Lammich, P.: Efficient verified implementation of Introsort and Pdqsort. In: Peltier, N., Sofronie-Stokkermans, V. (eds.) IJCAR 2020. LNCS (LNAI), vol. 12167, pp. 307\u2013323. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_18"},{"key":"24_CR13","doi-asserted-by":"publisher","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","DOI":"10.1109\/MS.2017.4121212"},{"key":"24_CR14","doi-asserted-by":"publisher","unstructured":"Leroy, X.: A formally verified compiler back-end. J. Autom. Reason. 43(4), 363\u2013446 (2009). https:\/\/doi.org\/10.1007\/s10817-009-9155-4","DOI":"10.1007\/s10817-009-9155-4"},{"key":"24_CR15","doi-asserted-by":"publisher","unstructured":"Mai, H., Pek, E., Xue, H., King, S.T., Madhusudan, P.: Verifying security invariants in expressos. In: Sarkar, V., Bod\u00edk, R. (eds.) Architectural Support for Programming Languages and Operating Systems, ASPLOS 2013, Houston, TX, USA, 16\u201320 March 2013, pp. 293\u2013304. ACM (2013). https:\/\/doi.org\/10.1145\/2451116.2451148","DOI":"10.1145\/2451116.2451148"},{"key":"24_CR16","unstructured":"Matias, M.: Program verification of FreeRTOS using Microsoft Dafny. Cleveland State University (2014). https:\/\/books.google.com.au\/books?id=A_iyoQEACAAJ"},{"key":"24_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction \u2013 CADE-25","author":"L de Moura","year":"2015","unstructured":"de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378\u2013388. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26"},{"key":"24_CR18","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":"24_CR19","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"424","DOI":"10.1007\/11532231_31","volume-title":"Automated Deduction \u2013 CADE-20","author":"M Ogawa","year":"2005","unstructured":"Ogawa, M., Horita, E., Ono, S.: Proving properties of incremental Merkle trees. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 424\u2013440. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11532231_31"},{"key":"24_CR20","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":"24_CR21","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":"24_CR22","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":"24_CR23","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":"24_CR24","doi-asserted-by":"publisher","unstructured":"Pe\u00f1a, R.: An assertional proof of red-black trees using Dafny. J. Autom. Reason. 64(4), 767\u2013791 (2020). https:\/\/doi.org\/10.1007\/s10817-019-09534-y","DOI":"10.1007\/s10817-019-09534-y"},{"key":"24_CR25","unstructured":"Runtime Verification Inc.: Formally verified smart contracts. https:\/\/github.com\/runtimeverification\/verified-smart-contracts"},{"key":"24_CR26","doi-asserted-by":"publisher","unstructured":"Sternagel, C.: Proof pearl-a mechanized proof of GHC\u2019s Mergesort. J. Autom. Reason. 51(4), 357\u2013370 (2013). https:\/\/doi.org\/10.1007\/s10817-012-9260-7","DOI":"10.1007\/s10817-012-9260-7"},{"key":"24_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-319-89960-2_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S Wimmer","year":"2018","unstructured":"Wimmer, S., Lammich, P.: Verified model checking of timed automata. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 61\u201378. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_4"},{"key":"24_CR28","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"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-90870-6_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,10]],"date-time":"2021-11-10T00:10:53Z","timestamp":1636503053000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-90870-6_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030908690","9783030908706"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-90870-6_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"10 November 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","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":"20 November 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 November 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/formalmethods2021.csp.escience.cn\/dct\/page\/1","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":"131","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":"40","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":"2","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":"31% - 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":"9","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)"}},{"value":"Additionally, this includes 4 invited full papers.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}