Skip to main content
SpringerLink
Log in
Book cover

From Software Engineering to Formal Methods and Tools, and Back pp 397–415Cite as

On the Prediction of Smart Contracts’ Behaviours

  • Chapter
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11865))

Abstract

Smart contracts are pieces of software stored on the blockchain that control the transfer of assets between parties under certain conditions. In this paper we analyze the bahaviour of smart contracts and the interaction with external actors in order to maximize objective functions. We define a core language of programs with a minimal set of smart contract primitives and we describe the whole system as a parallel composition of smart contracts and users. We therefore express the system behaviour as a first logic formula in Presburger arithmetics and study the maximum profit for each actor by solving arithmetic constraints.

Research partly supported by the H2020-MSCA-RISE project ID 778233 “Behavioural Application Program Interfaces (BEHAPI)”.

This is a preview of subscription content, 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   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.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

Learn about institutional subscriptions

References

  1. Asirelli, P., ter Beek, M.H., Fantechi, A., Gnesi, S.: A model-checking tool for families of services. In: Bruni, R., Dingel, J. (eds.) FMOODS/FORTE -2011. LNCS, vol. 6722, pp. 44–58. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21461-5_3

    Chapter  Google Scholar 

  2. Bhargavan, K., et al.: Formal verification of smart contracts: short paper. In: Proceedings of Programming Languages and Analysis for Security, pp. 91–96. ACM (2016)

    Google Scholar 

  3. Bigi, G., Bracciali, A., Meacci, G., Tuosto, E.: Validation of decentralised smart contracts through game theory and formal methods. In: Bodei, C., Ferrari, G.-L., Priami, C. (eds.) Programming Languages with Applications to Biology and Security. LNCS, vol. 9465, pp. 142–161. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-25527-9_11

    Chapter  MATH  Google Scholar 

  4. Chatterjee, K., Goharshady, A.K., Velner, Y.: Quantitative analysis of smart contracts. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 739–767. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89884-1_26

    Chapter  Google Scholar 

  5. Demri, S.: Linear-time temporal logics with presburger constraints: an overview. J. Appl. Non-Class. Logics 16(3–4), 311–348 (2006)

    Article  MathSciNet  Google Scholar 

  6. Ethereum Foundation. Ethereum’s white paper (2014). https://github.com/ ethereum/wiki/wiki/White-Paper

  7. Ethereum Foundation. Solidity 0.4.24 documentation (2019). https://solidity.readthedocs.io/en/develop/

  8. Ganesh, V., Berezin, S., Dill, D.L.: Deciding presburger arithmetic by model checking and comparisons with other methods. In: Aagaard, M.D., O’Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 171–186. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-36126-X_11

    Chapter  Google Scholar 

  9. Haase, C.: A survival guide to presburger arithmetic. ACM SIGLOG News 5(3), 67–82 (2018)

    Google Scholar 

  10. Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: Proceedings of the Conference on Computer and Communications Security, pp. 254–269. ACM (2016)

    Google Scholar 

  11. Mueller, B.: Smashing Ethereum smart contracts for fun and real profit. HITB SECCONF Amsterdam (2018)

    Google Scholar 

  12. Pnueli, A.: The temporal logic of programs. In: Proceedings of Symposium on Foundations of Computer Science. IEEE Computer Society, pp. 46–57 (1977)

    Google Scholar 

  13. Pope, J.: Formalizing constructive quantifier elimination in Agda. In: Proceedings of MSFP@FSCD 2018 of EPTCS, vol. 275, pp. 2–17 (2018)

    Google Scholar 

  14. OCamlPro SAS. Welcome to Liquidity’s documentation! (2019). http://www.liquidity-lang.org/doc/

  15. Siegel, D.: Understanding the DAO attack (2016). Accessed 13 Jun 2018

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science and Engineering, University of Bologna – INRIA Focus, Bologna, Italy

    Cosimo Laneve, Claudio Sacerdoti Coen & Adele Veschetti

Authors
  1. Cosimo Laneve
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Claudio Sacerdoti Coen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Adele Veschetti
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Cosimo Laneve .

Editor information

Editors and Affiliations

  1. Consiglio Nazionale delle Ricerche, Pisa, Italy

    Maurice H. ter Beek

  2. Università degli Studi di Firenze, Florence, Italy

    Alessandro Fantechi

  3. Università di Pisa, Pisa, Italy

    Laura Semini

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Laneve, C., Coen, C.S., Veschetti, A. (2019). On the Prediction of Smart Contracts’ Behaviours. In: ter Beek, M., Fantechi, A., Semini, L. (eds) From Software Engineering to Formal Methods and Tools, and Back. Lecture Notes in Computer Science(), vol 11865. Springer, Cham. https://doi.org/10.1007/978-3-030-30985-5_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-30985-5_23

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-30984-8

  • Online ISBN: 978-3-030-30985-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation