{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,27]],"date-time":"2026-05-27T13:10:16Z","timestamp":1779887416007,"version":"3.53.1"},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030309848","type":"print"},{"value":"9783030309855","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-30985-5_23","type":"book-chapter","created":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T21:53:39Z","timestamp":1570571619000},"page":"397-415","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["On the Prediction of Smart Contracts\u2019 Behaviours"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0052-4061","authenticated-orcid":false,"given":"Cosimo","family":"Laneve","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4360-6016","authenticated-orcid":false,"given":"Claudio Sacerdoti","family":"Coen","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0403-1889","authenticated-orcid":false,"given":"Adele","family":"Veschetti","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,10,9]]},"reference":[{"key":"23_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"44","DOI":"10.1007\/978-3-642-21461-5_3","volume-title":"Formal Techniques for Distributed Systems","author":"P Asirelli","year":"2011","unstructured":"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\u201358. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21461-5_3"},{"key":"23_CR2","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., et al.: Formal verification of smart contracts: short paper. In: Proceedings of Programming Languages and Analysis for Security, pp. 91\u201396. ACM (2016)","DOI":"10.1145\/2993600.2993611"},{"key":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-319-25527-9_11","volume-title":"Programming Languages with Applications to Biology and Security","author":"G Bigi","year":"2015","unstructured":"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\u2013161. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25527-9_11"},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"739","DOI":"10.1007\/978-3-319-89884-1_26","volume-title":"Programming Languages and Systems","author":"K Chatterjee","year":"2018","unstructured":"Chatterjee, K., Goharshady, A.K., Velner, Y.: Quantitative analysis of smart contracts. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 739\u2013767. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_26"},{"issue":"3\u20134","key":"23_CR5","doi-asserted-by":"publisher","first-page":"311","DOI":"10.3166\/jancl.16.311-347","volume":"16","author":"S Demri","year":"2006","unstructured":"Demri, S.: Linear-time temporal logics with presburger constraints: an overview. J. Appl. Non-Class. Logics 16(3\u20134), 311\u2013348 (2006)","journal-title":"J. Appl. Non-Class. Logics"},{"key":"23_CR6","unstructured":"Ethereum Foundation. Ethereum\u2019s white paper (2014). https:\/\/github.com\/ ethereum\/wiki\/wiki\/White-Paper"},{"key":"23_CR7","unstructured":"Ethereum Foundation. Solidity 0.4.24 documentation (2019). https:\/\/solidity.readthedocs.io\/en\/develop\/"},{"key":"23_CR8","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/3-540-36126-X_11","volume-title":"FMCAD 2002","author":"V Ganesh","year":"2002","unstructured":"Ganesh, V., Berezin, S., Dill, D.L.: Deciding presburger arithmetic by model checking and comparisons with other methods. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol. 2517, pp. 171\u2013186. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-36126-X_11"},{"issue":"3","key":"23_CR9","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1145\/3242953.3242964","volume":"5","author":"C Haase","year":"2018","unstructured":"Haase, C.: A survival guide to presburger arithmetic. ACM SIGLOG News 5(3), 67\u201382 (2018)","journal-title":"ACM SIGLOG News"},{"key":"23_CR10","doi-asserted-by":"crossref","unstructured":"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\u2013269. ACM (2016)","DOI":"10.1145\/2976749.2978309"},{"key":"23_CR11","unstructured":"Mueller, B.: Smashing Ethereum smart contracts for fun and real profit. HITB SECCONF Amsterdam (2018)"},{"key":"23_CR12","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of Symposium on Foundations of Computer Science. IEEE Computer Society, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"23_CR13","doi-asserted-by":"crossref","unstructured":"Pope, J.: Formalizing constructive quantifier elimination in Agda. In: Proceedings of MSFP@FSCD 2018 of EPTCS, vol. 275, pp. 2\u201317 (2018)","DOI":"10.4204\/EPTCS.275.2"},{"key":"23_CR14","unstructured":"OCamlPro SAS. Welcome to Liquidity\u2019s documentation! (2019). http:\/\/www.liquidity-lang.org\/doc\/"},{"key":"23_CR15","unstructured":"Siegel, D.: Understanding the DAO attack (2016). Accessed 13 Jun 2018"}],"container-title":["Lecture Notes in Computer Science","From Software Engineering to Formal Methods and Tools, and Back"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-30985-5_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,1,24]],"date-time":"2021-01-24T10:32:37Z","timestamp":1611484357000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-30985-5_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030309848","9783030309855"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-30985-5_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"9 October 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}