The dream of trustless transactions on blockchains has only been partially achieved. One of the worst gaps is the need to trust code, especially smart contracts. Breathtaking financial losses from exploited bugs in smart contracts, such as the DAO and Parity hacks, demonstrate this point. Bugs in smart contracts may be the most important limiting factor to mainstream adoption of blockchain technology.

True transparency cannot be achieved even by disclosing full source code, because subtle bugs and vulnerabilities in plain sight slip through careful inspection and testing.

I will describe methods for automatically verifying the code smart contracts.

My research focuses on easing the task of developing reliable and efficient software systems. I am particularly interested in static program analysis which combines two disciplines: automated theorem proving and abstract interpretation. In the next decade, I am hoping to develop useful techniques in order to change the ways modern software is built. I am particularly interested in proof automation, given a program and a requirement, automatically prove or disprove that all executions of the program satisfy the requirements. This problem is in general undecidable and untractable. I am interested in developing practical solutions to proof-automation by: (i) exploring modularity of the system and (ii) relying on semi-automatic and interactive process, where the user manually and interactively guides the proof automation, and (iii) simplifying the verification task by using domain-specific abstractions expressed in a decidable logic. I am applying these techniques to verify safety of liveness of distributed systems.