Formal Verification of EVM Bytecode

I’m a research engineer in the Trustworthy Smart Contracts Team at ConsenSys. My current focus is on the application of formal methods to smart contracts. Before that, I was an Associate Professor in the School of Engineering and Computer Science at Victoria University of Wellington, NZ. I graduated from the Department of Computing at Imperial College London, and moved to New Zealand in 2004. My research interests are in programming languages, compilers, static analysis and formal verification. I am the author of the Whiley programming language which (like Dafny) supports formal verification of functional specifications (i.e. preconditions / postconditions). Several of algorithms I have developed have found widespread use. For example, my algorithm for field-sensitive pointer analysis is used in GCC and godoc for Go; my algorithm for dynamic topological sort is used in Abseil and TensorFlow; another for finding strongly connected components is used in SciPy; finally, my algorithm for computing Tutte Polynomials features in both Mathematica and Sage. Finally, during my time as a PhD student I was an intern at Bell Labs, New Jersey, working on compilers for FPGAs and also at IBM Hursley, UK, working with the AspectJ development team on profiling systems.