Fast and Reliable Formal Verification of Smart Contracts with the Move Prover
- Open Access
- 2022
- OriginalPaper
- Buchkapitel
- Verfasst von
- David Dill
- Wolfgang Grieskamp
- Junkil Park
- Shaz Qadeer
- Meng Xu
- Emma Zhong
- Verlag
- Springer International Publishing
Zusammenfassung
The Move Prover (MVP) is a formal verifier for smart contracts written in the Move programming language. MVP 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 MVP: (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 MVP in a few minutes. Changes in the Diem framework must be successfully verified before being integrated into the open source repository on GitHub.
- Titel
- Fast and Reliable Formal Verification of Smart Contracts with the Move Prover
- Verfasst von
-
David Dill
Wolfgang Grieskamp
Junkil Park
Shaz Qadeer
Meng Xu
Emma Zhong
- Copyright-Jahr
- 2022
- Buch
-
Tools and Algorithms for the Construction and Analysis of Systems
Print ISBN: 978-3-030-99523-2
Electronic ISBN: 978-3-030-99524-9
Copyright-Jahr: 2022
- DOI
- https://doi.org/10.1007/978-3-030-99524-9_10
