{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,7]],"date-time":"2026-10-07T03:00:49Z","timestamp":1791342049113,"version":"4.3.1"},"publisher-location":"Cham","reference-count":32,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030995232","type":"print"},{"value":"9783030995249","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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T00:00:00Z","timestamp":1648598400000},"content-version":"vor","delay-in-days":88,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The Move Prover () is a formal verifier for smart contracts written in the Move programming language.  has an expressive specification language, and is fast and reliable enough that it can be run routinely by developers and in integration testing. Besides the simplicity of smart contracts and the Move language, three implementation approaches are responsible for the practicality of : (1) an alias-free memory model, (2) fine-grained invariant checking, and (3) monomorphization. The entirety of the Move code for the Diem blockchain has been extensively specified and can be completely verified by  in a few minutes. Changes in the Diem framework must be successfully verified before being integrated into the open source repository on GitHub.<\/jats:p>","DOI":"10.1007\/978-3-030-99524-9_10","type":"book-chapter","created":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:14:55Z","timestamp":1648534495000},"page":"183-200","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":19,"title":["Fast and Reliable Formal Verification of Smart Contracts with the Move Prover"],"prefix":"10.1007","author":[{"given":"David","family":"Dill","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Wolfgang","family":"Grieskamp","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Junkil","family":"Park","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Shaz","family":"Qadeer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Meng","family":"Xu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Emma","family":"Zhong","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2022,3,30]]},"reference":[{"key":"10_CR1","doi-asserted-by":"crossref","unstructured":"Astrauskas, V., M\u00fcller, P., Poli, F., Summers, A.J.: Leveraging rust types for modular specification and verification. PACMPL 3(OOPSLA), 147:1\u2013147:30 (2019)","DOI":"10.1145\/3360573"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Baranowski, M.S., He, S., Rakamaric, Z.: Verifying rust programs with SMACK. In: ATVA. Lecture Notes in Computer Science, vol. 11138, pp. 528\u2013535. Springer (2018)","DOI":"10.1007\/978-3-030-01090-4_32"},{"key":"10_CR3","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: International Symposium on Formal Methods for Components and Objects. pp. 364\u2013387. Springer (2005)","DOI":"10.1007\/11804192_17"},{"key":"10_CR4","doi-asserted-by":"crossref","unstructured":"Barnett, M., DeLine, R., F\u00e4hndrich, M., Jacobs, B., Leino, K.R.M., Schulte, W., Venter, H.: The Spec# Programming System: Challenges and Directions, pp. 144\u2013152. Springer Berlin Heidelberg, Berlin, Heidelberg (2008), https:\/\/doi.org\/10.1007\/978-3-540-69149-5_16","DOI":"10.1007\/978-3-540-69149-5_16"},{"key":"10_CR5","doi-asserted-by":"publisher","unstructured":"Clarke, D., \u00d6stlund, J., Sergey, I., Wrigstad, T.: Ownership types: A survey. In: Clarke, D., Noble, J., Wrigstad, T. (eds.) Aliasing in Object-Oriented Programming. Types, Analysis and Verification, Lecture Notes in Computer Science, vol.\u00a07850, pp. 15\u201358. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-36946-9_3","DOI":"10.1007\/978-3-642-36946-9_3"},{"key":"10_CR6","unstructured":"ConsenSys: Mythril Classic: Security analysis tool for Ethereum smart contracts, https:\/\/github.com\/skylightcyber\/mythril-classic"},{"key":"10_CR7","unstructured":"Dill, D.L., Grieskamp, W., Park, J., Qadeer, S., Xu, M., Zhong, J.E.: Fast and reliable formal verification of smart contracts with the move prover (extended version). CoRR abs\/2110.08362 (2021), https:\/\/arxiv.org\/abs\/2110.08362"},{"key":"10_CR8","unstructured":"Foundation, E.: Solidity documentation (2018), http:\/\/solidity.readthedocs.io"},{"key":"10_CR9","doi-asserted-by":"crossref","unstructured":"Hajdu, \u00c1., Jovanovic, D.: solc-verify: A modular verifier for solidity smart contracts. CoRR abs\/1907.04262 (2019)","DOI":"10.1007\/978-3-030-41600-3_11"},{"key":"10_CR10","doi-asserted-by":"crossref","unstructured":"Hajdu, \u00c1., Jovanovic, D.: SMT-Friendly Formalization of the Solidity Memory Model. In: ESOP. Lecture Notes in Computer Science, vol. 12075, pp. 224\u2013250. Springer (2020)","DOI":"10.1007\/978-3-030-44914-8_9"},{"key":"10_CR11","doi-asserted-by":"publisher","unstructured":"Leino, K.M.: Accessible software verification with dafny. IEEE Software 34(06), 94\u201397 (nov 2017). https:\/\/doi.org\/10.1109\/MS.2017.4121212","DOI":"10.1109\/MS.2017.4121212"},{"key":"10_CR12","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M., Pit-Claudel, C.: Trigger Selection Strategies to Stabilize Program Verifiers. In: Proceedings of the 28th International Conference on Computer Aided Verification, Part I. pp. 361\u2013381. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_20","DOI":"10.1007\/978-3-319-41528-4_20"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Lindner, M., Aparicius, J., Lindgren, P.: No panic! verification of rust programs by symbolic execution. In: INDIN. pp. 108\u2013114. IEEE (2018)","DOI":"10.1109\/INDIN.2018.8471992"},{"key":"10_CR14","doi-asserted-by":"crossref","unstructured":"Liu, J., Liu, Z.: A survey on security verification of blockchain smart contracts. IEEE Access 7, 77894\u201377904 (2019)","DOI":"10.1109\/ACCESS.2019.2921624"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Luu, L., Chu, D., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: ACM Conference on Computer and Communications Security. pp. 254\u2013269. ACM (2016)","DOI":"10.1145\/2976749.2978309"},{"key":"10_CR16","doi-asserted-by":"publisher","unstructured":"Matsakis, N.D., Klock, II, F.S.: The Rust Language, nourl = http:\/\/doi.acm.org\/10.1145\/2692956.2663188. Ada Lett. 34(3), 103\u2013104 (Oct 2014). https:\/\/doi.org\/10.1145\/2692956.2663188","DOI":"10.1145\/2692956.2663188"},{"key":"10_CR17","unstructured":"Meng Xu: Artifact for Paper \u201cFast and Reliable Formal Verification of Smart Contracts with the Move Prover\u201d (2020), https:\/\/github.com\/meng-xu-cs\/mvp-artifact"},{"key":"10_CR18","doi-asserted-by":"publisher","unstructured":"Meyer, B.: Applying \"design by contract\". Computer 25(10), 40\u201351 (Oct 1992). https:\/\/doi.org\/10.1109\/2.161279","DOI":"10.1109\/2.161279"},{"key":"10_CR19","unstructured":"Morisander: The Biggest Smart Contract Hacks in History Or How to Endanger up to US \\$2.2 Billion. https:\/\/medium.com\/solidified\/the-biggest-smart-contract-hacks-in-history-or-how-to-endanger-up-to-us-2-2-billion-d5a72961d15d (2018)"},{"key":"10_CR20","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: TACAS. Lecture Notes in Computer Science, vol.\u00a04963, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Nikolic, I., Kolluri, A., Sergey, I., Saxena, P., Hobor, A.: Finding the greedy, prodigal, and suicidal contracts at scale. In: ACSAC. pp. 653\u2013663. ACM (2018)","DOI":"10.1145\/3274694.3274743"},{"key":"10_CR22","unstructured":"Sigalos, M.: Bug Puts \\$162 Million up for Grabs, Says Founder of DeFi Platform Compound. https:\/\/www.cnbc.com\/2021\/10\/03\/162-million-up-for-grabs-after-bug-in-defi-protocol-compound-.html (2021)"},{"key":"10_CR23","unstructured":"The CVC Team: CVC5, https:\/\/github.com\/cvc5\/cvc5"},{"key":"10_CR24","unstructured":"The Diem Association: An Introduction to Diem (2019), https:\/\/www.diem.com\/en-us\/"},{"key":"10_CR25","unstructured":"The Diem Association: The Diem Framework (2020), https:\/\/github.com\/diem\/diem\/tree\/release-1.5\/diem-move\/diem-framework"},{"key":"10_CR26","unstructured":"The Move Team: The Move Programming Language (2020), https:\/\/diem.github.io\/move"},{"key":"10_CR27","unstructured":"The Move Team: The Move Specification Language (2020), https:\/\/github.com\/diem\/diem\/blob\/release-1.5\/language\/move-prover\/doc\/user\/spec-lang.md"},{"key":"10_CR28","unstructured":"Tillmann, N., Grieskamp, W., Schulte, W.: Efficient checking of state-dependent constraints (US Patent 20050198621A1, 2004)"},{"key":"10_CR29","unstructured":"Tolmach, P., Li, Y., Lin, S., Liu, Y., Li, Z.: A survey of smart contract formal specification and verification. CoRR abs\/2008.02712 (2020), https:\/\/arxiv.org\/abs\/2008.02712"},{"key":"10_CR30","doi-asserted-by":"crossref","unstructured":"Toman, J., Pernsteiner, S., Torlak, E.: Crust: A bounded verifier for rust (N). In: ASE. pp. 75\u201380. IEEE Computer Society (2015)","DOI":"10.1109\/ASE.2015.77"},{"key":"10_CR31","doi-asserted-by":"crossref","unstructured":"Tsankov, P., Dan, A.M., Drachsler-Cohen, D., Gervais, A., B\u00fcnzli, F., Vechev, M.T.: Securify: Practical security analysis of smart contracts. In: ACM Conference on Computer and Communications Security. pp. 67\u201382. ACM (2018)","DOI":"10.1145\/3243734.3243780"},{"key":"10_CR32","doi-asserted-by":"crossref","unstructured":"Zhong, J.E., Cheang, K., Qadeer, S., Grieskamp, W., Blackshear, S., Park, J., Zohar, Y., Barrett, C., Dill, D.L.: The Move Prover. In: Lahiri, S.K., Wang, C. (eds.) Computer Aided Verification. pp. 137\u2013150. Springer International Publishing (2020)","DOI":"10.1007\/978-3-030-53288-8_7"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-99524-9_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T06:20:31Z","timestamp":1648534831000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99524-9_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030995232","9783030995249"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99524-9_10","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":"30 March 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","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":"2 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/tacas","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":"159","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":"46","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":"4","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":"29% - 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":"10","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":"16 tool papers of the affiliated competition SV-Comp and 1 paper consisting of the competition report are also included in the proceedings","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)"}}]}}