{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T09:21:20Z","timestamp":1743067280119,"version":"3.40.3"},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030324087"},{"type":"electronic","value":"9783030324094"}],"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-32409-4_8","type":"book-chapter","created":{"date-parts":[[2019,10,27]],"date-time":"2019-10-27T20:03:00Z","timestamp":1572206580000},"page":"121-137","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Towards Verifying Ethereum Smart Contracts at Intermediate Language Level"],"prefix":"10.1007","author":[{"given":"Ximeng","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhiping","family":"Shi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Qianying","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guohui","family":"Wang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yong","family":"Guan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ning","family":"Han","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,10,28]]},"reference":[{"key":"8_CR1","unstructured":"CertiK. \n                      https:\/\/certik.org\/"},{"key":"8_CR2","unstructured":"ERC20 standard. \n                      https:\/\/theethereum.wiki\/w\/index.php\/ERC20_Token_Standard"},{"key":"8_CR3","unstructured":"Eth-isabelle. \n                      https:\/\/github.com\/pirapira\/eth-isabelle"},{"key":"8_CR4","unstructured":"Solidity (v0.5.8). \n                      https:\/\/solidity.readthedocs.io\/en\/v0.5.8\/"},{"key":"8_CR5","unstructured":"Token libraries with proofs. \n                      https:\/\/github.com\/sec-bit\/tokenlibs-with-proofs"},{"key":"8_CR6","unstructured":"Understanding the DAO attack. \n                      http:\/\/www.coindesk.com\/understanding-dao-hack-journalists\/"},{"key":"8_CR7","unstructured":"VaaS. \n                      https:\/\/sso.beosin.com\/#\/?vaas"},{"key":"8_CR8","unstructured":"Yul. \n                      https:\/\/solidity.readthedocs.io\/en\/v0.5.8\/yul.html"},{"key":"8_CR9","doi-asserted-by":"crossref","unstructured":"Amani, S., B\u00e9gel, M., Bortin, M., Staples, M.: Towards verifying Ethereum smart contract bytecode in Isabelle\/HOL. In: 7th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), pp. 66\u201377 (2018)","DOI":"10.1145\/3176245.3167084"},{"issue":"4","key":"8_CR10","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"KR Apt","year":"1981","unstructured":"Apt, K.R.: Ten years of Hoare\u2019s logic: a survey - part 1. ACM Trans. Program. Lang. Syst. 3(4), 431\u2013483 (1981)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on Ethereum smart contracts (SoK). In: 6th International Conference on Principles of Security and Trust (POST), pp. 164\u2013186 (2017)","DOI":"10.1007\/978-3-662-54455-6_8"},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Bai, X., Cheng, Z., Duan, Z., Hu, K.: Formal modeling and verification of smart contracts. In: 7th International Conference on Software and Computer Applications (ICSCA), pp. 322\u2013326 (2018)","DOI":"10.1145\/3185089.3185138"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Banach, R.: Verification-led smart contracts. In: Proceedings of 3rd Workshop on Trusted Smart Contracts (2019)","DOI":"10.1007\/978-3-658-27963-9_2"},{"key":"8_CR14","unstructured":"Beckert, B., Herda, M., Kirsten, M., Schiffl, J.: Formal specification and verification of Hyperledger Fabric chaincode. In: Third Symposium on Distributed Ledger Technology (SDLT) (2018)"},{"issue":"6","key":"8_CR15","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010)","journal-title":"J. Comput. Secur."},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-319-96145-3_4","volume-title":"Computer Aided Verification","author":"I Grishchenko","year":"2018","unstructured":"Grishchenko, I., Maffei, M., Schneidewind, C.: Foundations and tools for the static analysis of Ethereum smart contracts. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 51\u201378. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-96145-3_4"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-319-89722-6_10","volume-title":"Principles of Security and Trust","author":"I Grishchenko","year":"2018","unstructured":"Grishchenko, I., Maffei, M., Schneidewind, C.: A semantic framework for the security analysis of Ethereum smart contracts. In: Bauer, L., K\u00fcsters, R. (eds.) POST 2018. LNCS, vol. 10804, pp. 243\u2013269. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-89722-6_10"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Hildenbrandt, E., et al.: KEVM: a complete formal semantics of the Ethereum virtual machine. In: 31st IEEE Computer Security Foundations Symposium (CSF), pp. 204\u2013217 (2018)","DOI":"10.1109\/CSF.2018.00022"},{"key":"8_CR19","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). \n                      https:\/\/doi.org\/10.1007\/978-3-319-70278-0_33"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"Kalra, S., Goel, S., Dhawan, M., Sharma, S.: ZEUS: analyzing safety of smart contracts. In: 25th Network and Distr. System Security Symposium (NDSS) (2018)","DOI":"10.14722\/ndss.2018.23082"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"Luu, L., Chu, D., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: ACM SIGSAC Conference on Computer and Communications Security (CCS), pp. 254\u2013269 (2016)","DOI":"10.1145\/2976749.2978309"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"Owens, S., B\u00f6hm, P., Nardelli, F. Z., Sewell, P.: Lem: a lightweight tool for heavyweight semantics. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 363\u2013369. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-22863-6_27","DOI":"10.1007\/978-3-642-22863-6_27"},{"key":"8_CR23","doi-asserted-by":"crossref","unstructured":"Park, D., Zhang, Y., Saxena, M., Daian, P., Rosu, G.: A formal verification tool for Ethereum VM bytecode. In: ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/SIGSOFT (FSE), pp. 912\u2013915 (2018)","DOI":"10.1145\/3236024.3264591"},{"key":"8_CR24","unstructured":"Sergey, I., Kumar, A., Hobor, A.: Scilla: a smart contract intermediate-level language. CoRR, abs\/1801.00687 (2018)"},{"key":"8_CR25","unstructured":"Szabo, N.: Smart contracts (1994). \n                      http:\/\/www.fon.hum.uva.nl\/rob\/Courses\/InformationInSpeech\/CDROM\/Literature\/LOTwinterschool2006\/szabo.best.vwh.net\/smart.contracts.html"},{"key":"8_CR26","doi-asserted-by":"crossref","unstructured":"Tsankov, P., Dan, A.M., Drachsler-Cohen, D., Gervais, A., B\u00fcnzli, F., Vechev, M.T.: Securify: practical security analysis of smart contracts. In: ACM SIGSAC Conference on Computer and Communications Security (CCS), pp. 67\u201382 (2018)","DOI":"10.1145\/3243734.3243780"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-71067-7_7","volume-title":"Theorem Proving in Higher Order Logics","author":"M Wenzel","year":"2008","unstructured":"Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle framework. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 33\u201338. Springer, Heidelberg (2008). \n                      https:\/\/doi.org\/10.1007\/978-3-540-71067-7_7"},{"key":"8_CR28","unstructured":"Wood, G.: Ethereum: a secure decentralised generlised transaction ledger. \n                      https:\/\/gavwood.com\/paper.pdf"},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"Yaga, D., Mell, P., Roby, N., Scarfone, K.: Blockchain technology overview. Technical report, NISTIR 8202 (2018)","DOI":"10.6028\/NIST.IR.8202"},{"key":"8_CR30","unstructured":"Yang, Z., Lei, H.: Lolisa: formal syntax and semantics for a subset of the solidity programming language. CoRR, abs\/1803.09885 (2018)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-32409-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,11,2]],"date-time":"2019-11-02T04:54:05Z","timestamp":1572670445000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-32409-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030324087","9783030324094"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-32409-4_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"28 October 2019","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":"Shenzhen","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":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 November 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 November 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"icfem2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/csse.szu.edu.cn\/icfem2019\/","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":"94","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":"28","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":"0","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":"30% - 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":"3","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":"4","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)"}}]}}