Show simple item record

dc.rights.licenseCC-BY-NC-ND
dc.contributor.advisorSwierstra, W.S.
dc.contributor.authorMelkonian, O.
dc.date.accessioned2019-07-24T17:01:40Z
dc.date.available2019-07-24T17:01:40Z
dc.date.issued2019
dc.identifier.urihttps://studenttheses.uu.nl/handle/20.500.12932/32981
dc.description.abstractSmart contracts – programs that run on a blockchain – allow for sophisticated transactional schemes, but their concurrent execution makes it difficult to reason about their behaviour and bugs in smart contracts have lead to significant monetary losses (e.g. DAO attack). For that reason, increasingly more attention is given to formal methods, that guarantee that such fatal scenarios are not possible. We attempt to advance the state-of-the-art for a language-oriented, type-driven account of smart contracts by formalizing two well-established models in Agda and mechanizing the corresponding meta-theory. The first concerns an abstract model for UTxO-based ledgers, such as Bitcoin, which we further extend to cover features of the Cardano blockchain, namely more expressive scripts and built-in support for user-issued cryptocurrencies. The second object of study is BitML, a process calculus specifically targeting Bitcoin smart con- tracts. We present a mechanized semantics of BitML contracts and its small-step semantics, as well as a mechanized account of BitML’s symbolic model over participant strategies. Finally, we sketch the way towards a certified compiler from BitML contracts to UTxO transac- tions, where all behaviours manifesting on BitML’s symbolic model can safely be transported to the UTxO level.
dc.description.sponsorshipUtrecht University
dc.format.extent338918
dc.format.mimetypeapplication/pdf
dc.language.isoen
dc.titleFormalizing Extended UTxO and BitML Calculus in Agda
dc.type.contentMaster Thesis
dc.rights.accessrightsOpen Access
dc.subject.keywordsblockchain, smart contracts, operational semantics, formal verification, certified compilation, dependently-typed programming, Agda
dc.subject.courseuuComputing Science


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record