{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,10]],"date-time":"2026-07-10T17:56:50Z","timestamp":1783706210681,"version":"3.55.0"},"publisher-location":"New York, NY, USA","reference-count":21,"publisher":"ACM","license":[{"start":{"date-parts":[[2018,1,8]],"date-time":"2018-01-08T00:00:00Z","timestamp":1515369600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2018,1,8]]},"DOI":"10.1145\/3167084","type":"proceedings-article","created":{"date-parts":[[2018,3,16]],"date-time":"2018-03-16T16:10:56Z","timestamp":1521216656000},"page":"66-77","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":152,"title":["Towards verifying ethereum smart contract bytecode in Isabelle\/HOL"],"prefix":"10.1145","author":[{"given":"Sidney","family":"Amani","sequence":"first","affiliation":[{"name":"Data61 at CSIRO, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Myriam","family":"B\u00e9gel","sequence":"additional","affiliation":[{"name":"ENS Paris-Saclay, France \/ University of Paris-Saclay, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Maksym","family":"Bortin","sequence":"additional","affiliation":[{"name":"Data61 at CSIRO, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mark","family":"Staples","sequence":"additional","affiliation":[{"name":"Data61 at CSIRO, Australia \/ UNSW, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2018,1,8]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"2017. Securify. http:\/\/securify.ch .  2017. Securify. http:\/\/securify.ch ."},{"key":"e_1_3_2_1_2_1","volume-title":"Finite Machine Word Library. Archive of Formal Proofs (June","author":"Beeren Joel","year":"2016","unstructured":"Joel Beeren , Matthew Fernandez , Xin Gao , Gerwin Klein , Rafal Kolanski , Japheth Lim , Corey Lewis , Daniel Matichuk , and Thomas Sewell . 2016. Finite Machine Word Library. Archive of Formal Proofs (June 2016 ). http:\/\/isa-afp.org\/entries\/Word_Lib.html, Formal proof development. Joel Beeren, Matthew Fernandez, Xin Gao, Gerwin Klein, Rafal Kolanski, Japheth Lim, Corey Lewis, Daniel Matichuk, and Thomas Sewell. 2016. Finite Machine Word Library. Archive of Formal Proofs (June 2016). http:\/\/isa-afp.org\/entries\/Word_Lib.html, Formal proof development."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2993600.2993611"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_3_2_1_5_1","unstructured":"Ethereum foundation. 2017. Solidity documentation. https:\/\/solidity. readthedocs.io\/en\/develop\/ .  Ethereum foundation. 2017. Solidity documentation. https:\/\/solidity. readthedocs.io\/en\/develop\/ ."},{"key":"e_1_3_2_1_6_1","unstructured":"Ethereum foundation. 2017. Subroutines and Static Jumps for the EVM. https:\/\/github.com\/ethereum\/EIPs\/issues\/615 .  Ethereum foundation. 2017. Subroutines and Static Jumps for the EVM. https:\/\/github.com\/ethereum\/EIPs\/issues\/615 ."},{"key":"e_1_3_2_1_7_1","volume-title":"KEVM: A Complete Semantics of the Ethereum Virtual Machine . Technical Report.","author":"Hildenbrandt Everett","year":"2017","unstructured":"Everett Hildenbrandt , Manasvi Saxena , Xiaoran Zhu , Nishant Rodrigues , Philip Daian , Dwight Guth , and Grigore Rosu . 2017 . KEVM: A Complete Semantics of the Ethereum Virtual Machine . Technical Report. Everett Hildenbrandt, Manasvi Saxena, Xiaoran Zhu, Nishant Rodrigues, Philip Daian, Dwight Guth, and Grigore Rosu. 2017. KEVM: A Complete Semantics of the Ethereum Virtual Machine . Technical Report."},{"key":"e_1_3_2_1_8_1","volume-title":"1st Workshop on Trusted Smart Contracts, International Conference on Financial Cryprography and Data Security .","author":"Hirai Yoichi","year":"2017","unstructured":"Yoichi Hirai . 2017 . Defining the Ethereum Virtual Machine for Interactive Theorem Provers. In WTSC\u201917 , 1st Workshop on Trusted Smart Contracts, International Conference on Financial Cryprography and Data Security . Yoichi Hirai. 2017. Defining the Ethereum Virtual Machine for Interactive Theorem Provers. In WTSC\u201917, 1st Workshop on Trusted Smart Contracts, International Conference on Financial Cryprography and Data Security ."},{"key":"e_1_3_2_1_9_1","volume-title":"Mechanised Separation Algebra. In International Conference on Interactive Theorem Proving, Lennart Beringer and Amy Felty (Ed.). Springer","author":"Klein Gerwin","year":"2012","unstructured":"Gerwin Klein , Rafal Kolanski , and Andrew Boyton . 2012 . Mechanised Separation Algebra. In International Conference on Interactive Theorem Proving, Lennart Beringer and Amy Felty (Ed.). Springer , Princeton, USA, 332\u2013337. Gerwin Klein, Rafal Kolanski, and Andrew Boyton. 2012. Mechanised Separation Algebra. In International Conference on Interactive Theorem Proving, Lennart Beringer and Amy Felty (Ed.). Springer, Princeton, USA, 332\u2013337."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1146809.1146811"},{"key":"e_1_3_2_1_11_1","unstructured":"Xavier Leroy et al. 2012. The CompCert verified compiler. Documentation and user\u00e2\u0102\u0179s manual. INRIA Paris-Rocquencourt (2012).  Xavier Leroy et al. 2012. The CompCert verified compiler. Documentation and user\u00e2\u0102\u0179s manual. INRIA Paris-Rocquencourt (2012)."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978309"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9360-2"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628143"},{"key":"e_1_3_2_1_16_1","volume-title":"Lecture Notes in Computer Science","author":"Nipkow Tobias","unstructured":"Tobias Nipkow , Lawrence Paulson , and Markus Wenzel . 2002. Isabelle\/ HOL \u2014 A Proof Assistant for Higher-Order Logic . Lecture Notes in Computer Science , Vol. 2283 . Springer . Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. 2002. Isabelle\/HOL \u2014 A Proof Assistant for Higher-Order Logic . Lecture Notes in Computer Science, Vol. 2283. Springer."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110262"},{"key":"e_1_3_2_1_18_1","unstructured":"Christian Reitwiessner. 2016. Formal Verification of Smart Contracts. https:\/\/chriseth.github.io\/notes\/talks\/formal_ic3_bootcamp .  Christian Reitwiessner. 2016. Formal Verification of Smart Contracts. https:\/\/chriseth.github.io\/notes\/talks\/formal_ic3_bootcamp ."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_3_2_1_20_1","volume-title":"Porosity: A Decompiler For Blockchain-Based Smart Contracts Bytecode. https:\/\/github.com\/comaeio\/porosity\/blob\/ master\/defcon2017\/dc25-msuichePorosity-Decompiling-Ethereum-Smart-Contracts-wp.pdf .","author":"Suiche Matt","year":"2017","unstructured":"Matt Suiche . 2017 . Porosity: A Decompiler For Blockchain-Based Smart Contracts Bytecode. https:\/\/github.com\/comaeio\/porosity\/blob\/ master\/defcon2017\/dc25-msuichePorosity-Decompiling-Ethereum-Smart-Contracts-wp.pdf . Matt Suiche. 2017. Porosity: A Decompiler For Blockchain-Based Smart Contracts Bytecode. https:\/\/github.com\/comaeio\/porosity\/blob\/ master\/defcon2017\/dc25-msuichePorosity-Decompiling-Ethereum-Smart-Contracts-wp.pdf ."},{"key":"e_1_3_2_1_21_1","volume-title":"Ethereum: A secure decentralised generalised transaction ledger. Ethereum Project Yellow Paper 151","author":"Wood Gavin","year":"2014","unstructured":"Gavin Wood . 2014 . Ethereum: A secure decentralised generalised transaction ledger. Ethereum Project Yellow Paper 151 (2014). Gavin Wood. 2014. Ethereum: A secure decentralised generalised transaction ledger. Ethereum Project Yellow Paper 151 (2014)."},{"key":"e_1_3_2_1_22_1","volume-title":"Proc. 16th Conference of Japan Society for Software Science and Technology . 313\u2013316","author":"Zhao Jianjun","year":"1999","unstructured":"Jianjun Zhao . 1999 . Analyzing Control Flow in Java Bytecode . In Proc. 16th Conference of Japan Society for Software Science and Technology . 313\u2013316 . Jianjun Zhao. 1999. Analyzing Control Flow in Java Bytecode. In Proc. 16th Conference of Japan Society for Software Science and Technology . 313\u2013316."}],"event":{"name":"CPP '18: Certified Proofs and Programs","location":"Los Angeles CA USA","acronym":"CPP '18","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"]},"container-title":["Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3167084","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3167084","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:13:27Z","timestamp":1750212807000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3167084"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,8]]},"references-count":21,"alternative-id":["10.1145\/3167084","10.1145\/3176245"],"URL":"https:\/\/doi.org\/10.1145\/3167084","relation":{},"subject":[],"published":{"date-parts":[[2018,1,8]]},"assertion":[{"value":"2018-01-08","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}