Formal Specification and Verification of Smart Contracts
Smart contracts can be regarded as one of the most popular blockchain-based applications. The decentralized nature of blockchain introduces vulnerabilities absent in non-distributed programs. Furthermore, it is very difficult, if not impossible, to patch a smart contract after it is deployed. Therefore, smart contracts must be formally verified before they are deployed on the blockchain. In this work, we study the formal specification and verification of smart contracts.
- 1.Bhargavan, K., et al.: Formal verification of smart contracts. In: CCS 2016, pp. 91–96. ACM (2016)Google Scholar
- 3.Hildenbrandt, E., et al.: KEVM: a complete semantics of the Ethereum virtual machine, August 2017Google Scholar
- 4.Jiao, J., Kan, S., Lin, S., Sanán, D., Liu, Y., Sun, J.: Executable operational semantics of solidity. CoRR, abs/1804.01295 (2018)Google Scholar
- 5.Kalra, S., Goel, S., Dhawan, M., Sharma, S.: ZEUS: analyzing safety of smart contracts. In: NDSS 2018. The Internet Society (2018)Google Scholar
- 6.Luu, L., Chu, D., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: CCS 2016, pp. 254–269. ACM (2016)Google Scholar