{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,11]],"date-time":"2025-11-11T12:15:06Z","timestamp":1762863306700,"version":"3.40.3"},"publisher-location":"Singapore","reference-count":27,"publisher":"Springer Nature Singapore","isbn-type":[{"type":"print","value":"9789819606160"},{"type":"electronic","value":"9789819606177"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-981-96-0617-7_22","type":"book-chapter","created":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T14:47:11Z","timestamp":1732805231000},"page":"391-407","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Model Checking Concurrency in\u00a0Smart Contracts with\u00a0a\u00a0Case Study of\u00a0Safe Remote Purchase"],"prefix":"10.1007","author":[{"given":"Yisong","family":"Yu","sequence":"first","affiliation":[]},{"given":"Naipeng","family":"Dong","sequence":"additional","affiliation":[]},{"given":"Zhe","family":"Hou","sequence":"additional","affiliation":[]},{"given":"Jin","family":"Song Dong","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,11,29]]},"reference":[{"key":"22_CR1","unstructured":"Post-mortem investigation (2016). https:\/\/www.kingoftheether.com\/postmortem.html. Accessed 11 Apr 2024"},{"key":"22_CR2","doi-asserted-by":"publisher","DOI":"10.1016\/j.pmcj.2020.101227","volume":"67","author":"M Almakhour","year":"2020","unstructured":"Almakhour, M., Sliman, L., Samhat, A.E., Mellouk, A.: Verification of smart contracts: a survey. Pervasive Mob. Comput. 67, 101227 (2020)","journal-title":"Pervasive Mob. Comput."},{"key":"22_CR3","unstructured":"Angelo, M.D., Salzer, G.: A survey of tools for analyzing ethereum smart contracts. In: DAPPS, pp. 69\u201378 (2019)"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on ethereum smart contracts (sok). In: POST, pp. 164\u2013186 (2017)","DOI":"10.1007\/978-3-662-54455-6_8"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"Braghin, C., Riccobene, E., Valentini, S.: An asm-based approach for security assessment of ethereum smart contracts. In: SECRYPT, pp. 334\u2013344 (2024)","DOI":"10.5220\/0012858000003767"},{"key":"22_CR6","doi-asserted-by":"crossref","unstructured":"Braghin, C., Riccobene, E., Valentini, S.: Modeling and verification of smart contracts with abstract state machines. In: SAC, pp. 1425\u20131432 (2024)","DOI":"10.1145\/3605098.3636040"},{"key":"22_CR7","unstructured":"Braithwaite, S., et al.: Formal specification and model checking of the tendermint blockchain synchronization protocol (short paper). In: FMBC (2020)"},{"key":"22_CR8","unstructured":"Breidenbach, L., Juels, P.D.A., Sirer, E.G.: An in-depth look at the parity multisig bug (2017). https:\/\/hackingdistributed.com\/2017\/07\/22\/deep-dive-parity-bug\/. Accessed 11 Apr 2024"},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"Chen, H., Pendleton, M., Njilla, L., Xu, S.: A survey on ethereum systems security: vulnerabilities, attacks, and defenses. ACM Comput. Surv. 53(3) (2021)","DOI":"10.1145\/3391195"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"Daian, P., et al.: Flash boys 2.0: frontrunning in decentralized exchanges, miner extractable value, and consensus instability. In: SP, pp. 910\u2013927 (2020)","DOI":"10.1109\/SP40000.2020.00040"},{"key":"22_CR11","doi-asserted-by":"crossref","unstructured":"Grieco, G., Song, W., Cygan, A., Feist, J., Groce, A.: Echidna: effective, usable, and fast fuzzing for smart contracts. In: ISSTA, pp. 557\u2013560 (2020)","DOI":"10.1145\/3395363.3404366"},{"key":"22_CR12","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":"22_CR13","doi-asserted-by":"crossref","unstructured":"Luu, L., Chu, D., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: CCS, pp. 254\u2013269 (2016)","DOI":"10.1145\/2976749.2978309"},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"Maung Maung\u00a0Thin, W.Y., Dong, N., Bai, G., Dong, J.S.: Formal analysis of a proof-of-stake blockchain. In: ICECCS, pp. 197\u2013200 (2018)","DOI":"10.1109\/ICECCS2018.2018.00031"},{"key":"22_CR15","doi-asserted-by":"crossref","unstructured":"Munir, S., Reichenbach, C.: Todler: a transaction ordering dependency analyzer - for ethereum smart contracts. In: WETSEB, pp. 9\u201316 (2023)","DOI":"10.1109\/WETSEB59161.2023.00007"},{"key":"22_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-030-05764-0_4","volume-title":"Smart Blockchain","author":"M Qu","year":"2018","unstructured":"Qu, M., Huang, X., Chen, X., Wang, Y., Ma, X., Liu, D.: Formal verification of smart contracts from the perspective of concurrency. In: Qiu, M. (ed.) SmartBlock 2018. LNCS, vol. 11373, pp. 32\u201343. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-05764-0_4"},{"key":"22_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-319-70278-0_30","volume-title":"Financial Cryptography and Data Security","author":"I Sergey","year":"2017","unstructured":"Sergey, I., Hobor, A.: A concurrent perspective on smart contracts. In: Brenner, M., Rohloff, K., Bonneau, J., Miller, A., Ryan, P.Y.A., Teague, V., Bracciali, A., Sala, M., Pintore, F., Jakobsson, M. (eds.) FC 2017. LNCS, vol. 10323, pp. 478\u2013493. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-70278-0_30"},{"key":"22_CR18","unstructured":"Siegel, D.: Understanding the DAO attack. https:\/\/www.coindesk.com\/learn\/understanding-the-dao-attack\/. Accessed 11 Apr 2024"},{"key":"22_CR19","unstructured":"Solidity: Solidity by example safe remote purchase. https:\/\/docs.soliditylang.org\/en\/latest\/solidity-by-example.html. Accessed 16 Apr 2024"},{"key":"22_CR20","unstructured":"Sotnichek, M.: Formal verification of smart contracts with the k framework (2019). https:\/\/www.apriorit.com\/dev-blog\/592-formal-verification-with-k-framework. Accessed 23 Sept 2024"},{"key":"22_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1007\/978-3-642-02658-4_59","volume-title":"Computer Aided Verification","author":"J Sun","year":"2009","unstructured":"Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709\u2013714. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_59"},{"key":"22_CR22","doi-asserted-by":"crossref","unstructured":"Thin, W.Y.M.M., Dong, N., Bai, G., Dong, J.S.: Formal analysis of a proof-of-stake blockchain. In: ICECCS, pp. 197\u2013200 (2018)","DOI":"10.1109\/ICECCS2018.2018.00031"},{"key":"22_CR23","doi-asserted-by":"crossref","unstructured":"Tholoniat, P., Gramoli, V.: Formal verification of blockchain byzantine fault tolerance. In: Handbook on Blockchain, pp. 389\u2013412 (2022)","DOI":"10.1007\/978-3-031-07535-3_12"},{"key":"22_CR24","doi-asserted-by":"crossref","unstructured":"Tolmach, P., Li, Y., Lin, S., Liu, Y., Li, Z.: A survey of smart contract formal specification and verification. ACM Comput. Surv. 54(7), 148:1\u2013148:38 (2022)","DOI":"10.1145\/3464421"},{"key":"22_CR25","doi-asserted-by":"crossref","unstructured":"Wang, Y., Li, J., Liu, W., Tan, A., Derhab, A.: Efficient concurrent execution of smart contracts in blockchain sharding. Secur. Commun. Netw. (2021)","DOI":"10.1155\/2021\/6688168"},{"key":"22_CR26","unstructured":"Wood, G.: Ethereum: a secure decentralised generalised transaction ledger (2019). https:\/\/ethereum.github.io\/yellowpaper\/paper.pdf"},{"key":"22_CR27","doi-asserted-by":"crossref","unstructured":"Xu, X., Pautasso, C., Zhu, L., Lu, Q., Weber, I.: A pattern collection for blockchain-based applications. In: EuroPLoP, pp. 3:1\u20133:20 (2018)","DOI":"10.1145\/3282308.3282312"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-96-0617-7_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,28]],"date-time":"2024-11-28T15:10:02Z","timestamp":1732806602000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-96-0617-7_22"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9789819606160","9789819606177"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-981-96-0617-7_22","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"29 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICFEM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Formal Engineering Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Hiroshima","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Japan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 December 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 December 2024","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":"icfem2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.icfem2024.info\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}