Model Checking Upgrades in Ethereum Smart Contracts
Master thesis
View/ Open
Date
2023-06-02Metadata
Show full item recordCollections
- Master theses [203]
Abstract
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.