{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,11]],"date-time":"2025-07-11T10:24:51Z","timestamp":1752229491367,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030861612"},{"type":"electronic","value":"9783030861629"}],"license":[{"start":{"date-parts":[[2021,9,3]],"date-time":"2021-09-03T00:00:00Z","timestamp":1630627200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,9,3]],"date-time":"2021-09-03T00:00:00Z","timestamp":1630627200000},"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":[[2022]]},"DOI":"10.1007\/978-3-030-86162-9_1","type":"book-chapter","created":{"date-parts":[[2021,9,2]],"date-time":"2021-09-02T04:02:30Z","timestamp":1630555350000},"page":"3-13","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Formal Analysis of Smart Contracts: Model Impact Factor on Criminality"],"prefix":"10.1007","author":[{"given":"Malaw","family":"Ndiaye","sequence":"first","affiliation":[]},{"given":"Karim","family":"Konat\u00e9","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,9,3]]},"reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Abdellatif, T., Brousmiche, K.-L.: Formal verification of smart contracts based on users and blockchain behaviors models. In: 2018 9th IFIP International Conference on New Technologies, Mobility and Security (NTMS), pp. 1\u20135. IEEE (2018)","DOI":"10.1109\/NTMS.2018.8328737"},{"key":"1_CR2","doi-asserted-by":"crossref","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, pp. 66\u201377. ACM (2018)","DOI":"10.1145\/3167084"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"Bartoletti, M., Galletta, L., Murgia, M.: A true concurrent model of smart contracts executions. In: International Conference on Coordination Languages and Models, pp. 243\u2013260. Springer (2020)","DOI":"10.1007\/978-3-030-50029-0_16"},{"key":"1_CR4","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., et al.: Short paper: formal verification of smart contracts. In: Proceedings of the 11th ACM Workshop on Programming Languages and Analysis for Security (PLAS), in Conjunction with ACM CCS, pp. 91\u201396 (2016)","DOI":"10.1145\/2993600.2993611"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Bigi, G., Bracciali, A., Meacci, G., Tuosto, E.: Validation of decentralised smart contracts through game theory and formal methods. In: Programming Languages with Applications to Biology and Security, pp. 142\u2013161. Springer (2015)","DOI":"10.1007\/978-3-319-25527-9_11"},{"key":"1_CR6","unstructured":"Brent, L., et al.: Vandal: a scalable security analysis framework for smart contracts. arXiv preprint arXiv:1809.03981 (2018)"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Chen, W., Zheng, Z., Cui, J., Ngai, E., Zheng, P., Zhou, Y.: Detecting ponzi schemes on ethereum: towards healthier blockchain technology. In: Proceedings of the 2018 World Wide Web Conference, pp. 1409\u20131418 (2018)","DOI":"10.1145\/3178876.3186046"},{"key":"1_CR8","doi-asserted-by":"crossref","unstructured":"Di Angelo, M., Salzer, G.: A survey of tools for analyzing ethereum smart contracts. In: 2019 IEEE International Conference on Decentralized Applications and Infrastructures (DAPPCON). IEEE (2019)","DOI":"10.1109\/DAPPCON.2019.00018"},{"key":"1_CR9","unstructured":"Dika, A.: Ethereum smart contracts: Security vulnerabilities and security tools. Master\u2019s thesis, NTNU (2017)"},{"issue":"2","key":"1_CR10","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1108\/IJCS-03-2019-0010","volume":"3","author":"T Feng","year":"2019","unstructured":"Feng, T., Yu, X., Chai, Y., Liu, Y.: Smart contract model for complex reality transaction. Int. J. Crowd Sci. 3(2), 184\u2013197 (2019). https:\/\/doi.org\/10.1108\/IJCS-03-2019-0010","journal-title":"Int. J. Crowd Sci."},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Fu, Y., et al.: EVMFuzzer: detect EVM vulnerabilities via fuzz testing. In Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 1110\u20131114. ACM (2019)","DOI":"10.1145\/3338906.3341175"},{"key":"1_CR12","doi-asserted-by":"crossref","unstructured":"Hadjidj, R., Yang, X., Tlili, S., Debbabi, M.: Model-checking for software vulnerabilities detection with multi-language support. In: 2008 Sixth Annual Conference on Privacy, Security and Trust, pp. 133\u2013142. IEEE (2008)","DOI":"10.1109\/PST.2008.21"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"He, J., Balunovi\u0107, M., Ambroladze, N., Tsankov, P., Vechev, M.: Learning to fuzz from symbolic execution with application to smart contracts. In: Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, pp. 531\u2013548 (2019)","DOI":"10.1145\/3319535.3363230"},{"key":"1_CR14","unstructured":"Hirai, Y.: Formal verification of deed contract in ethereum name service, November 2016 (2016). https:\/\/yoichihirai.com\/deed.pdf"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Jiang, B., Liu, Y., Chan, W.K.: ContractFuzzer: fuzzing smart contracts for vulnerability detection. In: Proceedings of the 33rd ACM\/IEEE International Conference on Automated Software Engineering, pp. 259\u2013269. ACM (2018)","DOI":"10.1145\/3238147.3238177"},{"key":"1_CR16","first-page":"54","volume":"40","author":"A Juels","year":"2015","unstructured":"Juels, A., Kosba, A., Shi, E.: The ring of gyges: using smart contracts for crime. Aries 40, 54 (2015)","journal-title":"Aries"},{"key":"1_CR17","doi-asserted-by":"crossref","unstructured":"Juels, A., Kosba, A., Shi, E.: The ring of gyges: investigating the future of criminal smart contracts. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, pp. 283\u2013295 (2016)","DOI":"10.1145\/2976749.2978362"},{"key":"1_CR18","doi-asserted-by":"crossref","unstructured":"Kalra, S., Goel, S., Dhawan, M., Sharma, S.: Analyzing safety of smart contracts. In: NDSS, Zeus (2018)","DOI":"10.14722\/ndss.2018.23082"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Lamport, L.: \u201cSometime\u201d is sometimes \u201cnot never\u201d on the temporal logic of programs. In: Proceedings of the 7th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 174\u2013185 (1980)","DOI":"10.1145\/567446.567463"},{"key":"1_CR20","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 (2016)","DOI":"10.1145\/2976749.2978309"},{"key":"1_CR21","doi-asserted-by":"crossref","unstructured":"Murray, Y., Anisi, D.A.: Survey of formal verification methods for smart contracts on blockchain. In: 2019 10th IFIP International Conference on New Technologies, Mobility and Security (NTMS), pp. 1\u20136. IEEE (2019)","DOI":"10.1109\/NTMS.2019.8763832"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Nehai, Z., Piriou, P.-Y., Daumas, F.: Model-checking of smart contracts. In: 2018 IEEE International Conference on Internet of Things (iThings) and IEEE Green Computing and Communications (GreenCom) and IEEE Cyber, Physical and Social Computing (CPSCom) and IEEE Smart Data (SmartData), pp. 980\u2013987. IEEE (2018)","DOI":"10.1109\/Cybermatics_2018.2018.00185"},{"key":"1_CR23","doi-asserted-by":"crossref","unstructured":"Nguyen, Q.-B. Nguyen, A.-Q., Nguyen, V.-H., Nguyen-Le, T., Nguyen-An, K.: Detect abnormal behaviours in ethereum smart contracts using attack vectors. In: International Conference on Future Data and Security Engineering, pp. 485\u2013505. Springer (2019)","DOI":"10.1007\/978-3-030-35653-8_32"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Nguyen, T.D., Pham, L.H., Sun, J., Lin, Y., Minh, Q.T.: sFuzz: an efficient adaptive fuzzer for solidity smart contracts. arXiv preprint arXiv:2004.08563 (2020)","DOI":"10.1145\/3377811.3380334"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Nikolic, 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":"1_CR26","first-page":"18","volume":"110","author":"T Osterland","year":"2017","unstructured":"Osterland, T., Rose, T.: Correctness of smart contracts for consistency enforcement. ERCIM NEWS 110, 18\u201319 (2017)","journal-title":"ERCIM NEWS"},{"key":"1_CR27","unstructured":"Parizi, R.M., Dehghantanha, A., Choo, K.-K.R., Singh, A.: Empirical vulnerability analysis of automated smart contracts security testing on blockchains. In: Proceedings of the 28th Annual International Conference on Computer Science and Software Engineering, pp. 103\u2013113. IBM Corp. (2018)"},{"key":"1_CR28","doi-asserted-by":"crossref","unstructured":"Permenev, A., Dimitrov, D., Tsankov, P., Drachsler-Cohen, D., Vechev, M.: VerX: safety verification of smart contracts. In: 2020 IEEE Symposium on Security and Privacy, SP, pp. 18\u201320 (2020)","DOI":"10.1109\/SP40000.2020.00024"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"1_CR30","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: 2004 Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science, pp. 32\u201341. IEEE (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"1_CR31","doi-asserted-by":"crossref","unstructured":"So, S., Lee, M., Park, J., Lee, H., Oh, H.: VeriSmart: a highly precise safety verifier for ethereum smart contracts. In: 2020 IEEE Symposium on Security and Privacy (SP), pp. 1678\u20131694. IEEE (2020)","DOI":"10.1109\/SP40000.2020.00032"},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"Torres, C.F., Sch\u00fctte, J., State, R.: Osiris: hunting for integer bugs in ethereum smart contracts. In: Proceedings of the 34th Annual Computer Security Applications Conference, pp. 664\u2013676 (2018)","DOI":"10.1145\/3274694.3274737"},{"key":"1_CR33","doi-asserted-by":"crossref","unstructured":"Wang, H., Li, Y., Lin, S.-W., Ma, L., Liu, Y.: VULTRON: catching vulnerable smart contracts once and for all. In: Proceedings of the 41st International Conference on Software Engineering: New Ideas and Emerging Results, pp. 1\u20134. IEEE Press (2019)","DOI":"10.1109\/ICSE-NIER.2019.00009"},{"issue":"11","key":"1_CR34","doi-asserted-by":"publisher","first-page":"2266","DOI":"10.1109\/TSMC.2019.2895123","volume":"49","author":"S Wang","year":"2019","unstructured":"Wang, S., Ouyang, L., Yuan, Y., Ni, X., Han, X., Wang, F.-Y.: Blockchain-enabled smart contracts: architecture, applications, and future trends. IEEE Trans. Syst. Man Cybern.: Syst. 49(11), 2266\u20132277 (2019)","journal-title":"IEEE Trans. Syst. Man Cybern.: Syst."},{"key":"1_CR35","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/j.ins.2018.10.057","volume":"477","author":"Y Wang","year":"2019","unstructured":"Wang, Y., Bracciali, A., Li, T., Li, F., Cui, X., Zhao, M.: Randomness invalidates criminal smart contracts. Inf. Sci. 477, 291\u2013301 (2019)","journal-title":"Inf. Sci."},{"key":"1_CR36","unstructured":"Wood, G.: Ethereum: a secure decentralized generalized transaction ledger (EIP-150 revision) (2020). http:\/\/gavwood.com\/paper.pdf"},{"key":"1_CR37","doi-asserted-by":"crossref","unstructured":"Wustholz, V., Christakis, M.: Harvey: a greybox fuzzer for smart contracts. arXiv preprint arXiv:1905.06944 (2019)","DOI":"10.1145\/3368089.3417064"},{"key":"1_CR38","doi-asserted-by":"crossref","unstructured":"Xia, X., Ji, Q., Le, J.: Research on transaction dependency mechanism of self-healing database system. In: 2012 International Conference on Systems and Informatics (ICSAI2012), pp. 2357\u20132360. IEEE (2012)","DOI":"10.1109\/ICSAI.2012.6223528"}],"container-title":["Lecture Notes in Networks and Systems","Blockchain and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-86162-9_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,9,2]],"date-time":"2021-09-02T04:05:47Z","timestamp":1630555547000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-86162-9_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,9,3]]},"ISBN":["9783030861612","9783030861629"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-86162-9_1","relation":{},"ISSN":["2367-3370","2367-3389"],"issn-type":[{"type":"print","value":"2367-3370"},{"type":"electronic","value":"2367-3389"}],"subject":[],"published":{"date-parts":[[2021,9,3]]},"assertion":[{"value":"3 September 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"BLOCKCHAIN","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Congress on Blockchain and Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Salamanca","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 October 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 October 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"blockchain2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.blockchain-congress.net\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}