Formal Specification and Verification of Smart Contracts

  • Jiao JiaoEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11852)


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. 1.
    Bhargavan, K., et al.: Formal verification of smart contracts. In: CCS 2016, pp. 91–96. ACM (2016)Google Scholar
  2. 2.
    Grishchenko, I., Maffei, M., Schneidewind, C.: A semantic framework for the security analysis of Ethereum smart contracts. In: Bauer, L., Küsters, R. (eds.) POST 2018. LNCS, vol. 10804, pp. 243–269. Springer, Cham (2018). Scholar
  3. 3.
    Hildenbrandt, E., et al.: KEVM: a complete semantics of the Ethereum virtual machine, August 2017Google Scholar
  4. 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. 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. 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

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.School of Computer Science and EngineeringNanyang Technological UniversitySingaporeSingapore

Personalised recommendations