@inproceedings{db303f389dd243a1a104599bfd21a5e5,
title = "A formal verification tool for ethereum VM bytecode",
abstract = "In this paper, we present a formal verification tool for the Ethereum Virtual Machine (EVM) bytecode. To precisely reason about all possible behaviors of the EVM bytecode, we adopted KEVM, a complete formal semantics of the EVM, and instantiated the Kframework's reachability logic theorem prover to generate a correctby- construction deductive verifier for the EVM. We further optimized the verifier by introducing EVM-specific abstractions and lemmas to improve its scalability. Our EVM verifier has been used to verify various high-profile smart contracts including the ERC20 token, Ethereum Casper, and DappHub MakerDAO contracts.",
keywords = "Ethereum, K framework, formal verification, smart contracts",
author = "Daejun Park and Yi Zhang and Manasvi Saxena and Philip Daian and Grigore Ro{\c s}u",
note = "Publisher Copyright: {\textcopyright} 2018 Association for Computing Machinery.; 26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2018 ; Conference date: 04-11-2018 Through 09-11-2018",
year = "2018",
month = oct,
day = "26",
doi = "10.1145/3236024.3264591",
language = "English (US)",
series = "ESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering",
publisher = "Association for Computing Machinery",
pages = "912--915",
editor = "Alessandro Garci and Pasareanu, {Corina S.} and Leavens, {Gary T.}",
booktitle = "ESEC/FSE 2018 - Proceedings of the 2018 26th ACM Joint Meeting on European So ftware Engineering Conference and Symposium on the Foundations of So ftware Engineering",
address = "United States",
}