Skip to main content
SpringerLink
Log in

Formal-Verification of Smart-Contract Languages: A Survey

  • Conference paper
  • First Online:
Advances in Computing and Data Sciences (ICACDS 2019)

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 1046))

Included in the following conference series:

Abstract

A blockchain is a peer-to-peer electronic ledger of transactions that may be publicly or privately distributed to all users. Apart from unique consensus mechanisms, their success is also obliged to smart contracts. Also, These programs let on distrusting parties to enter reconciliation that are executed autonomously. Although a number of studies focus on security of introducing new programming languages., However, there is no comprehensive survey on the smart-contract language in suitability and expressiveness concepts and properties that recognize the interaction between people in organizations and technology in workplaces. To fill this gap, we conduct a systematic analysis about smart-contract language properties that focus on e-contractual and pattern-based exploration. In particular, this paper gives smart-contract language taxonomy, introducing technical challenges of languages as well as recent solutions in tackling the challenges. Moreover, this paper also represents the future research direction in the introducing new smart-contract language.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on ethereum smart contracts (SoK). In: Maffei, M., Ryan, M. (eds.) POST 2017. LNCS, vol. 10204, pp. 164–186. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54455-6_8

    Chapter  Google Scholar 

  2. Bartoletti, M., Pompianu, L.: An empirical analysis of smart contracts: platforms, applications, and design patterns. In: Brenner, M., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 494–509. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-70278-0_31

    Chapter  Google Scholar 

  3. Buterin, V., et al.: A next-generation smart contract and decentralized application platform. White paper (2014)

    Google Scholar 

  4. Christensen, L.B.: Experimental Methodology. Allyn & Bacon, Boston (2004)

    Google Scholar 

  5. ConsenSys: trufflesuite/truffle (2015). https://github.com/trufflesuite/truffle. Accessed 3 Mar 2018

  6. Ethereum: ethereum/solidity (2015). https://github.com/ethereum/solidity. Accessed 3 Mar 2018

  7. Giancaspro, M.: Is a ‘smart contract’ really a smart idea? Insights from a legal perspective. Comput. Law Secur. Rev. 33(6), 825–835 (2017)

    Article  Google Scholar 

  8. Knuth, D.E.: Semantics of context-free languages. Math. Syst. Theory 2(2), 127–145 (1968)

    Article  MathSciNet  Google Scholar 

  9. March, S.T., Storey, V.C.: Design science in the information systems discipline: an introduction to the special issue on design science research. MIS Q. 32, 725–730 (2008)

    Article  Google Scholar 

  10. Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008)

    Google Scholar 

  11. Norta, A., Ma, L., Duan, Y., Rull, A., Kõlvart, M., Taveter, K.: eContractual choreography-language properties towards cross-organizational business collaboration. J. Internet Serv. Appl. 6(1), 8 (2015)

    Article  Google Scholar 

  12. Norta, A.H.: Exploring dynamic inter-organizational business process collaboration. Dissertation Abstracts International, 68(04) (2007)

    Google Scholar 

  13. RChain: RChain/rholang. https://steemit.com/smart/@alexbafana/smart-contract-languages-comparison

  14. Roxenhall, T., Ghauri, P.: Use of the written contract in long-lasting business relationships. Ind. Mark. Manag. 33(3), 261–268 (2004)

    Article  Google Scholar 

  15. Sein, M.K., Henfridsson, O., Purao, S., Rossi, M., Lindgren, R.: Action design research. MIS Q. 35, 37–56 (2011)

    Article  Google Scholar 

  16. Singh, M.P., Chopra, A.K.: Violable contracts and governance for blockchain applications. arXiv preprint arXiv:1801.02672 (2018)

  17. Szabo, N.: Formalizing and securing relationships on public networks. First Monday 2(9) (1997)

    Google Scholar 

  18. Weber, I., Xu, X., Riveret, R., Governatori, G., Ponomarev, A., Mendling, J.: Untrusted business process monitoring and execution using blockchain. In: La Rosa, M., Loos, P., Pastor, O. (eds.) BPM 2016. LNCS, vol. 9850, pp. 329–347. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-45348-4_19

    Chapter  Google Scholar 

Download references

Acknowledgement

This Ph.D. research is partially supported by Quantum Foundation, Singapore under the supervision of Prof. Alex Norta, Associate Professor, Department of Software Science, Tallinn University of Technology, Tallinn, Estonia. Email: alex.norta.phd@ieee.org We thank our Prof. Alex Norta who provided insight and expertise that greatly assisted the research.

Author information

Authors and Affiliations

  1. Department of Software Science, Tallinn University of Technology, Akadeemia tee 15A, 12816, Tallinn, Estonia

    Vimal Dwivedi, Vipin Deval, Abhishek Dixit & Alex Norta

Authors
  1. Vimal Dwivedi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Vipin Deval
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Abhishek Dixit
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Alex Norta
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Vimal Dwivedi .

Editor information

Editors and Affiliations

  1. University of KwaZulu-Natal, Durban, South Africa

    Mayank Singh

  2. Computer Science and Engineering, Jaypee Institute of Information Technology, Waknaghat, Himachal Pradesh, India

    P.K. Gupta

  3. Department of Computer Science and Engineering, Jaypee University of Engineering and Technology, Guna, Madhya Pradesh, India

    Vipin Tyagi

  4. ÚTIA AV ČR, Institute of Information Theory and Automation, Prague 8, Praha, Czech Republic

    Jan Flusser

  5. School of Electrical Engineering and Computer Science, University of Ottawa, Ottawa, ON, Canada

    Tuncer Ören

  6. CSE Department, Inderprastha Engineering College, Ghaziabad, Uttar Pradesh, India

    Rekha Kashyap

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Singapore Pte Ltd.

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Dwivedi, V., Deval, V., Dixit, A., Norta, A. (2019). Formal-Verification of Smart-Contract Languages: A Survey. In: Singh, M., Gupta, P., Tyagi, V., Flusser, J., Ören, T., Kashyap, R. (eds) Advances in Computing and Data Sciences. ICACDS 2019. Communications in Computer and Information Science, vol 1046. Springer, Singapore. https://doi.org/10.1007/978-981-13-9942-8_68

Download citation

  • DOI: https://doi.org/10.1007/978-981-13-9942-8_68

  • Published:

  • Publisher Name: Springer, Singapore

  • Print ISBN: 978-981-13-9941-1

  • Online ISBN: 978-981-13-9942-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation