{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:03:32Z","timestamp":1760043812459,"version":"3.40.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030628215"},{"type":"electronic","value":"9783030628222"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-62822-2_2","type":"book-chapter","created":{"date-parts":[[2020,11,8]],"date-time":"2020-11-08T21:04:28Z","timestamp":1604869468000},"page":"17-34","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Reentrancy? Yes. Reentrancy Bug? No."],"prefix":"10.1007","author":[{"given":"Qinxiang","family":"Cao","sequence":"first","affiliation":[]},{"given":"Zhongye","family":"Wang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,11,9]]},"reference":[{"key":"2_CR1","unstructured":"Solidity - Solidity 053 documentation. https:\/\/solidity.readthedocs.io\/en\/v0.5.3\/"},{"key":"2_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-98047-8_1","volume-title":"Principled Software Development","author":"W Ahrendt","year":"2018","unstructured":"Ahrendt, W., Pace, G.J., Schneider, G.: Smart contracts: a killer application for deductive source code verification. Principled Software Development, pp. 1\u201318. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-98047-8_1"},{"key":"2_CR3","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\/3176245.3167084"},{"key":"2_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-19718-5_1","volume-title":"Programming Languages and Systems","author":"AW Appel","year":"2011","unstructured":"Appel, A.W.: Verified software toolchain. In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 1\u201317. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19718-5_1"},{"key":"2_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-745-5","volume-title":"Verification of Sequential and Concurrent Programs","author":"K Apt","year":"2010","unstructured":"Apt, K., De Boer, F.S., Olderog, E.R.: Verification of Sequential and Concurrent Programs. Springer, London (2010). https:\/\/doi.org\/10.1007\/978-1-84882-745-5"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-662-54455-6_8","volume-title":"Principles of Security and Trust","author":"N Atzei","year":"2017","unstructured":"Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on ethereum smart contracts (SoK). In: Maffei, M., Ryan, M. (eds.) POST 2017. LNCS, vol. 10204, pp. 164\u2013186. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54455-6_8"},{"key":"2_CR7","unstructured":"Barras, B., et al.: The Coq Proof Assistant reference manual. Technical report, INRIA (1998)"},{"key":"2_CR8","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":"2_CR9","unstructured":"Buterin, V., et al.: A next-generation smart contract and decentralized application platform. white paper, vol. 3, p. 37 (2014)"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Cao, Q., Wang, Z.: Reentrancy? Yes. Reentrancy bug? No (2020). https:\/\/archive.org\/details\/paper_reentry","DOI":"10.1007\/978-3-030-62822-2_2"},{"key":"2_CR11","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/s10817-018-9457-5","volume":"61","author":"Q Cao","year":"2018","unstructured":"Cao, Q., Beringer, L., Gruetter, S., Dodds, J., Appel, A.W.: VST-Floyd: a separation logic tool to verify correctness of C programs. J. Autom. Reason. 61, 367\u2013422 (2018)","journal-title":"J. Autom. Reason."},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Chen, H., Pendleton, M., Njilla, L., Xu, S.: A survey on ethereum systems security: Vulnerabilities, attacks and defenses. arXiv preprint arXiv:1908.04507 (2019)","DOI":"10.1145\/3391195"},{"key":"2_CR13","unstructured":"ConsenSys. https:\/\/consensys.github.io\/smart-contract-best-practices\/known_attacks\/ (Ethereum Smart Contract Best Practices: Known Attacks)"},{"key":"2_CR14","unstructured":"Cook, T., Latham, A., Lee, J.H.: DappGuard: Active monitoring and defense for solidity smart contracts (2017). Accessed 18 July 2018"},{"key":"2_CR15","doi-asserted-by":"crossref","unstructured":"Grossman, S., Abraham, I., Golan-Gueta, G., Michalevsky, Y., Rinetzky, N., Sagiv, M., Zohar, Y.: Online detection of effectively callback free objects with applications to smart contracts. In: Proceedings of the ACM on Programming Languages, vol. 2, no. POPL, p. 48 (2017)","DOI":"10.1145\/3158136"},{"key":"2_CR16","doi-asserted-by":"crossref","unstructured":"Hajdu, \u00c1., Jovanovi\u0107, D.: solc-verify: A modular verifier for solidity smart contracts. arXiv preprint arXiv:1907.04262 (2019)","DOI":"10.1007\/978-3-030-41600-3_11"},{"key":"2_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"520","DOI":"10.1007\/978-3-319-70278-0_33","volume-title":"Financial Cryptography and Data Security","author":"Y Hirai","year":"2017","unstructured":"Hirai, Y.: Defining the ethereum virtual machine for interactive theorem provers. In: Brenner, M., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 520\u2013535. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-70278-0_33"},{"issue":"10","key":"2_CR18","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 578\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"2_CR19","doi-asserted-by":"crossref","unstructured":"Kalra, S., Goel, S., Dhawan, M., Sharma, S.: Zeus: analyzing safety of smart contracts. In: NDSS (2018)","DOI":"10.14722\/ndss.2018.23082"},{"key":"2_CR20","unstructured":"Krebbers, R., Timany, A., Birkedal, L.: Interactive proofs in higher-order concurrent separation logic. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, 18\u201320 January 2017, pp. 205\u2013217. ACM (2017). http:\/\/dl.acm.org\/citation.cfm?id=3009855"},{"issue":"7","key":"2_CR21","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"2_CR22","unstructured":"Liu, C., Liu, H., Cao, Z., Chen, Z., Chen, B., Roscoe, B.: ReGuard: finding reentrancy bugs in smart contracts. In: Proceedings of the 40th International Conference on Software Engineering: Companion Proceeedings, ICSE 2018, pp. 65\u201368. ACM, New York (2018). http:\/\/doi.acm.org\/10.1145\/3183440.3183495"},{"key":"2_CR23","doi-asserted-by":"crossref","unstructured":"Nielsen, J.B., Spitters, B.: Smart contract interactions in coq. Submitted to FMBC19 (2019)","DOI":"10.1007\/978-3-030-54994-7_29"},{"key":"2_CR24","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., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 478\u2013493. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-70278-0_30"},{"key":"2_CR25","unstructured":"Siegel, D.: Understanding the DAO attack (2016). Accessed 13 June 2018"},{"key":"2_CR26","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":"2_CR27","unstructured":"Tan, G., Appel, A.W.: A compositional logic for control flow and its application in foundational proof-carrying code. Princeton University (2005)"},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"Wloka, J., Sridharan, M., Tip, F.: Refactoring for reentrancy. In: Proceedings of the the 7th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on The Foundations of Software Engineering, pp. 173\u2013182. ACM (2009)","DOI":"10.1145\/1595696.1595723"}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering. Theories, Tools, and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-62822-2_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,27]],"date-time":"2022-11-27T07:53:48Z","timestamp":1669535628000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-62822-2_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030628215","9783030628222"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-62822-2_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"9 November 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETTA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Dependable Software Engineering: Theories, Tools, and Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Guangzhou","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 November 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 November 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setta2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/lcs.ios.ac.cn\/setta2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"20","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"10","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"1","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"50% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}