{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,24]],"date-time":"2026-10-24T01:53:37Z","timestamp":1792806817358,"version":"4.5.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319702773","type":"print"},{"value":"9783319702780","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","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":[[2017]]},"DOI":"10.1007\/978-3-319-70278-0_33","type":"book-chapter","created":{"date-parts":[[2017,11,17]],"date-time":"2017-11-17T21:03:19Z","timestamp":1510952599000},"page":"520-535","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":204,"title":["Defining the Ethereum Virtual Machine for Interactive Theorem Provers"],"prefix":"10.1007","author":[{"given":"Yoichi","family":"Hirai","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2017,11,19]]},"reference":[{"key":"33_CR1","unstructured":"The Coq proof assistant. https:\/\/coq.inria.fr\/ . Accessed 19 Dec 2016"},{"key":"33_CR2","unstructured":"Ethereum VM tests. https:\/\/github.com\/ethereum\/tests\/tree\/develop\/VMTests . Accessed 02 Jan 2017"},{"key":"33_CR3","unstructured":"Solidity 0.4.8-develop documentation. https:\/\/solidity.readthedocs.io\/ . Accessed 19 Dec 2016"},{"key":"33_CR4","unstructured":"WebAssembly. http:\/\/webassembly.org\/ . Accessed 16 Dec 2016"},{"key":"33_CR5","unstructured":"Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on Ethereum smart contracts. Cryptology ePrint Archive (2016). http:\/\/eprint.iacr.org\/2016\/1007"},{"issue":"1","key":"33_CR6","doi-asserted-by":"crossref","first-page":"55","DOI":"10.1145\/1925844.1926394","volume":"46","author":"M Batty","year":"2011","unstructured":"Batty, M., Owens, S., Sarkar, S., Sewell, P., Weber, T.: Mathematizing C++ concurrency. SIGPLAN Not. 46(1), 55\u201366 (2011)","journal-title":"SIGPLAN Not."},{"key":"33_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-319-48989-6_5","volume-title":"FM 2016: Formal Methods","author":"H Becker","year":"2016","unstructured":"Becker, H., et al.: Combining mechanized proofs and model-based testing in the formal analysis of a hypervisor. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 69\u201384. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_5"},{"key":"33_CR8","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Delignat-Lavaud, A., Fournet, C., Gollamudi, A., Gonthier, G., Kobeissi, N., Kulatova, N., Rastogi, A., Sibut-Pinote, T., Swamy, N., Zanella-B\u00e9guelin, S.: Formal verification of smart contracts: short paper. In: PLAS 2016, pp. 91\u201396. ACM (2016)","DOI":"10.1145\/2993600.2993611"},{"issue":"1","key":"33_CR9","doi-asserted-by":"crossref","first-page":"166","DOI":"10.1145\/227595.227603","volume":"43","author":"RS Boyer","year":"1996","unstructured":"Boyer, R.S., Yu, Y.: Automated proofs of object code for a widely used microprocessor. J. ACM 43(1), 166\u2013192 (1996)","journal-title":"J. ACM"},{"key":"33_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/10930755_2","volume-title":"Theorem Proving in Higher Order Logics","author":"A Fox","year":"2003","unstructured":"Fox, A.: Formal specification and verification of ARM6. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 25\u201340. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/10930755_2"},{"key":"33_CR11","doi-asserted-by":"crossref","unstructured":"Kennedy, A., Benton, N., Jensen, J.B., Dagand, P.E.: Coq: the world\u2019s best macro assembler? In: PPDP 2013, pp. 13\u201324. ACM (2013)","DOI":"10.1145\/2505879.2505897"},{"issue":"4","key":"33_CR12","doi-asserted-by":"crossref","first-page":"619","DOI":"10.1145\/1146809.1146811","volume":"28","author":"G Klein","year":"2006","unstructured":"Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM Trans. Program. Lang. Syst. 28(4), 619\u2013695 (2006)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"33_CR13","doi-asserted-by":"crossref","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: POPL 2014, pp. 179\u2013191. ACM, New York (2014)","DOI":"10.1145\/2535838.2535841"},{"issue":"7","key":"33_CR14","doi-asserted-by":"crossref","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":"33_CR15","doi-asserted-by":"crossref","unstructured":"Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: CCS 2016, pp. 254\u2013269. ACM (2016)","DOI":"10.1145\/2976749.2978309"},{"issue":"9","key":"33_CR16","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1145\/2692915.2628143","volume":"49","author":"DP Mulligan","year":"2014","unstructured":"Mulligan, D.P., Owens, S., Gray, K.E., Ridge, T., Sewell, P.: Lem: reusable engineering of real-world semantics. SIGPLAN Not. 49(9), 175\u2013188 (2014)","journal-title":"SIGPLAN Not."},{"key":"33_CR17","first-page":"78","volume":"2012","author":"MO Myreen","year":"2012","unstructured":"Myreen, M.O., Gordon, M.J.C., Slind, K.: Decompilation into logic-improved. FMCAD 2012, 78\u201381 (2012)","journal-title":"FMCAD"},{"key":"33_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-540-75698-9_18","volume-title":"International Symposium on Fundamentals of Software Engineering","author":"MO Myreen","year":"2007","unstructured":"Myreen, M.O., Fox, A.C.J., Gordon, M.J.C.: Hoare logic for ARM machine code. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol. 4767, pp. 272\u2013286. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75698-9_18"},{"key":"33_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"33_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/978-3-662-49498-1_23","volume-title":"Programming Languages and Systems","author":"S Owens","year":"2016","unstructured":"Owens, S., Myreen, M.O., Kumar, R., Tan, Y.K.: Functional big-step semantics. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 589\u2013615. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_23"},{"issue":"1","key":"33_CR21","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1145\/1925844.1926395","volume":"46","author":"T Ramananandro","year":"2011","unstructured":"Ramananandro, T., Dos Reis, G., Leroy, X.: Formal verification of object layout for C++ multiple inheritance. SIGPLAN Not. 46(1), 67\u201380 (2011)","journal-title":"SIGPLAN Not."},{"issue":"6","key":"33_CR22","doi-asserted-by":"crossref","first-page":"397","DOI":"10.1016\/j.jlap.2010.03.012","volume":"79","author":"G Ro\u015fu","year":"2010","unstructured":"Ro\u015fu, G., \u015eerb\u0103nu\u0163\u0103, T.F.: An overview of the K semantic framework. J. Log. Algebr. Program. 79(6), 397\u2013434 (2010)","journal-title":"J. Log. Algebr. Program."},{"key":"33_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28\u201332. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_6"},{"key":"33_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/11609773_6","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"G Tan","year":"2005","unstructured":"Tan, G., Appel, A.W.: A compositional logic for control flow. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 80\u201394. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11609773_6"},{"key":"33_CR25","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1016\/j.entcs.2012.06.008","volume":"285","author":"F Wiedijk","year":"2012","unstructured":"Wiedijk, F.: Pollack-inconsistency. Electron. Notes Theor. Comput. Sci. 285, 85\u2013100 (2012)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"33_CR26","unstructured":"Wood, G.: Ethereum: a secure decentralised generalised transaction ledger-EIP-150 revision. http:\/\/paper.gavwood.com\/ . Accessed 19 Dec 2016"}],"container-title":["Lecture Notes in Computer Science","Financial Cryptography and Data Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-70278-0_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,6]],"date-time":"2019-10-06T05:19:04Z","timestamp":1570339144000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-70278-0_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319702773","9783319702780"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-70278-0_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}