Etherum smart contracts written in higher level programming languages like Solidity or Viper are compiled to bytecode, which is executed by the Ethereum Virtual Machine (EVM). Any instruction executed on the EVM has a monetary cost.

In this talk, I present our tool that automatically optimizes EVM bytecode. Our EVM Bytecode SuperOptimizer “<ahref=“https://github.com/juliannagele/ebso">ebso” implements (unbounded) superoptimization, which relies on an SMT solver to guarantee correctness of the transformation. We then perform a large scale evaluation of ebso on contracts deployed on the Etherum Blockchain.

This is joint work by Julian Nagele and <ahref=“http://maria-a-schett.net/">Maria A Schett.