Model Checking Upgrades in Ethereum Smart Contracts
Master thesis
Permanent lenke
https://hdl.handle.net/11250/3072558Utgivelsesdato
2023-06-02Metadata
Vis full innførselSamlinger
- Master theses [247]
Sammendrag
In this master’s thesis, the model-checking tool StraTegic Verifier has been extended to verify upgrades in Smart Contracts. It has been shown how to model Smart Contracts as Concurrent Game Models, enabling them to be verified by the model checker. By implementing Dictatorial Dynamic Coalition Logic, upgrades of Smart Contracts can be expressed, and the models can be changed before verification. The implementation of DDCL is a step in the direction of being able to use formal verification when there are upgrades in Smart Contracts.