{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,14]],"date-time":"2026-01-14T19:32:21Z","timestamp":1768419141330,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783662639573","type":"print"},{"value":"9783662639580","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-662-63958-0_30","type":"book-chapter","created":{"date-parts":[[2021,9,16]],"date-time":"2021-09-16T14:04:04Z","timestamp":1631801044000},"page":"364-380","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["EthVer: Formal Verification of Randomized Ethereum Smart Contracts"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3296-3138","authenticated-orcid":false,"given":"\u0141ukasz","family":"Mazurek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,9,17]]},"reference":[{"key":"30_CR1","unstructured":"Accidental bug may have frozen \\$280 million worth of digital coin ether in a cryptocurrency wallet. https:\/\/www.cnbc.com\/2017\/11\/08\/accidental-bug-may-have-frozen-280-worth-of-ether-on-parity-wallet.html. Accessed 2 Mar 2019"},{"key":"30_CR2","unstructured":"How to find \\$10m just by reading the blockchain. https:\/\/coinspectator.com\/news\/539\/how-to-find-10m-just-by-reading-the-blockchain. Accessed 2 Mar 2019"},{"key":"30_CR3","unstructured":"An in-depth look at the parity multisig bug. http:\/\/hackingdistributed.com\/2017\/07\/22\/deep-dive-parity-bug\/. Accessed 2 Mar 2019"},{"key":"30_CR4","unstructured":"Manticore. https:\/\/github.com\/trailofbits\/manticore"},{"key":"30_CR5","unstructured":"Mythril. https:\/\/github.com\/ConsenSys\/mythril"},{"key":"30_CR6","unstructured":"Smartcheck. https:\/\/github.com\/smartdec\/smartcheck"},{"key":"30_CR7","unstructured":"solgraph. https:\/\/github.com\/raineorshine\/solgraph"},{"key":"30_CR8","doi-asserted-by":"publisher","unstructured":"Amani, S., B\u00e9gel, M., Bortin, M., Staples, M.: Towards verifying ethereum smart contract bytecode in Isabelle\/HOL. In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018, pp. 66\u201377. ACM, New York (2018). https:\/\/doi.org\/10.1145\/3167084","DOI":"10.1145\/3167084"},{"key":"30_CR9","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., et al.: Formal verification of smart contracts: short paper. In: Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, pp. 91\u201396. ACM (2016)","DOI":"10.1145\/2993600.2993611"},{"key":"30_CR10","unstructured":"Buterin, V.: Ethereum: a next-generation smart contract and decentralized application platform (2014). https:\/\/github.com\/ethereum\/wiki\/wiki\/White-Paper. Accessed 22 Aug 2016"},{"key":"30_CR11","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"},{"key":"30_CR12","unstructured":"Cook, T., Latham, A., Lee, J.H.: Dappguard: active monitoring and defense for solidity smart contracts. Retrieved July 18, 2018 (2017)"},{"key":"30_CR13","series-title":"Communications in Computer and Information Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-662-44893-9_12","volume-title":"Cryptography and Security Systems","author":"NT Courtois","year":"2014","unstructured":"Courtois, N.T., Grajek, M., Naik, R.: Optimizing SHA256 in bitcoin mining. In: Kotulski, Z., Ksi\u0119\u017copolski, B., Mazur, K. (eds.) CSS 2014. CCIS, vol. 448, pp. 131\u2013144. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-662-44893-9_12"},{"key":"30_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/978-3-662-53357-4_6","volume-title":"Financial Cryptography and Data Security","author":"K Delmolino","year":"2016","unstructured":"Delmolino, K., Arnett, M., Kosba, A., Miller, A., Shi, E.: Step by step towards creating a safe smart contract: lessons and insights from a cryptocurrency lab. In: Clark, J., Meiklejohn, S., Ryan, P.Y.A., Wallach, D., Brenner, M., Rohloff, K. (eds.) FC 2016. LNCS, vol. 9604, pp. 79\u201394. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-53357-4_6"},{"key":"30_CR15","unstructured":"Falkon, S.: The story of the DAO \u2013 its history and consequences (2017). https:\/\/medium.com\/swlh\/the-story-of-the-dao-its-history-and-consequences-71e6a8a551ee"},{"key":"30_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"30_CR17","doi-asserted-by":"crossref","unstructured":"Grossman, S., et al.: Online detection of effectively callback free objects with applications to smart contracts. In: Proceedings of the ACM on Programming Languages 2(POPL), pp. 1\u201328 (2017)","DOI":"10.1145\/3158136"},{"key":"30_CR18","doi-asserted-by":"publisher","unstructured":"Hildenbrandt, E., et al.: Kevm: a complete formal semantics of the ethereum virtual machine. In: 2018 IEEE 31st Computer Security Foundations Symposium (CSF), pp. 204\u2013217 (2018). https:\/\/doi.org\/10.1109\/CSF.2018.00022","DOI":"10.1109\/CSF.2018.00022"},{"key":"30_CR19","doi-asserted-by":"crossref","unstructured":"Hirai, Y.: Defining the ethereum virtual machine for interactive theorem provers. In: Financial Cryptography Workshops (2017)","DOI":"10.1007\/978-3-319-70278-0_33"},{"key":"30_CR20","doi-asserted-by":"crossref","unstructured":"Kalra, S., Goel, S., Dhawan, M., Sharma, S.: Zeus: analyzing safety of smart contracts. In: NDSS, pp. 1\u201312 (2018)","DOI":"10.14722\/ndss.2018.23082"},{"key":"30_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"30_CR22","doi-asserted-by":"crossref","unstructured":"Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, pp. 254\u2013269. ACM (2016)","DOI":"10.1145\/2976749.2978309"},{"key":"30_CR23","unstructured":"Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system. http:\/\/bitcoin.org\/bitcoin.pdf"},{"key":"30_CR24","doi-asserted-by":"crossref","unstructured":"Nikoli\u0107, I., Kolluri, A., Sergey, I., Saxena, P., Hobor, A.: Finding the greedy, prodigal, and suicidal contracts at scale. In: Proceedings of the 34th Annual Computer Security Applications Conference, pp. 653\u2013663 (2018)","DOI":"10.1145\/3274694.3274743"},{"key":"30_CR25","doi-asserted-by":"crossref","unstructured":"O\u2019Connor, R.: Simplicity: a new language for blockchains. In: Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security, pp. 107\u2013120 (2017)","DOI":"10.1145\/3139337.3139340"},{"key":"30_CR26","doi-asserted-by":"publisher","unstructured":"Pass, R., Shelat, A.: Micropayments for decentralized currencies. In: Ray, I., Li, N., Kruegel, C. (eds.) ACM CCS 2015: 22nd Conference on Computer and Communications Security, pp. 207\u2013218. ACM Press, Denver (2015). https:\/\/doi.org\/10.1145\/2810103.2813713","DOI":"10.1145\/2810103.2813713"},{"key":"30_CR27","unstructured":"Pass, R., Shelat, A.: Micropayments for decentralized currencies. Cryptology ePrint Archive, Report 2016\/332 (2016). http:\/\/eprint.iacr.org\/2016\/332"},{"key":"30_CR28","unstructured":"Pettersson, J., Edstr\u00f6m, R.: Safer smart contracts through type-driven development. Master\u2019s thesis. Chalmers University of Technology, Sweden (2016)"},{"key":"30_CR29","doi-asserted-by":"crossref","unstructured":"Szabo, N.: Formalizing and securing relationships on public networks. First Monday 2(9) (1997)","DOI":"10.5210\/fm.v2i9.548"},{"key":"30_CR30","doi-asserted-by":"publisher","unstructured":"Tsankov, P., Dan, A., Drachsler-Cohen, D., Gervais, A., B\u00fcnzli, F., Vechev, M.: Security: practical security analysis of smart contracts. In: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, pp. 67\u201382. ACM, New York (2018). https:\/\/doi.org\/10.1145\/3243734.3243780","DOI":"10.1145\/3243734.3243780"},{"key":"30_CR31","doi-asserted-by":"crossref","unstructured":"Wohrer, M., Zdun, U.: Smart contracts: security patterns in the ethereum ecosystem and solidity. In: 2018 International Workshop on Blockchain Oriented Software Engineering (IWBOSE), pp. 2\u20138. IEEE (2018)","DOI":"10.1109\/IWBOSE.2018.8327565"},{"key":"30_CR32","doi-asserted-by":"crossref","unstructured":"Zhou, E., et al.: Security assurance for smart contract. In: 2018 9th IFIP International Conference on New Technologies, Mobility and Security (NTMS), pp. 1\u20135. IEEE (2018)","DOI":"10.1109\/NTMS.2018.8328743"}],"container-title":["Lecture Notes in Computer Science","Financial Cryptography and Data Security. FC 2021 International Workshops"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-63958-0_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,16]],"date-time":"2021-09-16T14:13:14Z","timestamp":1631801594000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-662-63958-0_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783662639573","9783662639580"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-63958-0_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"17 September 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Financial Cryptography and Data Security","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 March 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fc2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/fc21.ifca.ai\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}