Fragments of formal verification of the  Solidity smart contracts

dc.contributor.author	Shumakov, Maksym
dc.date.accessioned	2024-02-14T12:46:59Z
dc.date.available	2024-02-14T12:46:59Z
dc.date.issued	2022
dc.identifier.citation	Shumakov, Maksym. Fragments of formal verification of the Solidity smart contracts / Shumakov, Maksym; Supervisor: Vasyl Lenko; Ukrainian Catholic University, Department of Computer Sciences. – Lviv: 2022. – 36 p.	uk
dc.identifier.uri	https://er.ucu.edu.ua/handle/1/4445
dc.language.iso	en	uk
dc.title	Fragments of formal verification of the Solidity smart contracts	uk
dc.type	Preprint	uk
dc.status	Публікується вперше	uk
dc.description.abstracten	We present our elaborations on the software verification techniques using the Coq formal proof management system of the Solidity smart contracts. As modern Blockchain systems that provide smart contracts functionality often manage enormous amounts of valuable digital assets, it is significant to understand the inherent vulnerabilities of the system’s general architecture and implementation. We have confined our model only to Solidity and analogues depth-first execution blockchains. Our research con- siders the Safe Remote Purchase Solidity contract and modelled in Coq’s functional language Gallina.	uk