| dc.contributor.author | Aga, Eirin Maria Larsson | |
| dc.date.accessioned | 2023-06-22T00:02:23Z | |
| dc.date.available | 2023-06-22T00:02:23Z | |
| dc.date.issued | 2023-06-02 | |
| dc.date.submitted | 2023-06-21T22:01:19Z | |
| dc.identifier.uri | https://hdl.handle.net/11250/3072558 | |
| dc.description.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. | |
| dc.language.iso | eng | |
| dc.publisher | The University of Bergen | |
| dc.rights | Copyright the Author. All rights reserved | |
| dc.subject | Smart Contracts | |
| dc.subject | Coalition Logic | |
| dc.subject | Model Checking | |
| dc.title | Model Checking Upgrades in Ethereum Smart Contracts | |
| dc.type | Master thesis | |
| dc.date.updated | 2023-06-21T22:01:19Z | |
| dc.rights.holder | Copyright the Author. All rights reserved | |
| dc.description.degree | Masteroppgave i informasjonsvitenskap | |
| dc.description.localcode | INFO390 | |
| dc.description.localcode | MASV-INFO | |
| dc.subject.nus | 735115 | |
| fs.subjectcode | INFO390 | |
| fs.unitcode | 15-17-0 | |
