FORMAL VERIFICATION OF SMART CONTRACTS
Dr. Christian Reitwiessner
@ethchris
github.com/chriseth
IC3-Ethereum Crypto Boot Camp
2016-07-26
Problem:
Writing code correctly is hard!
Key goal: align mental model with machine model
Easy to test desired behaviour, hard to check absence of undesired behaviour
Reason: testing catches only finite amount of cases
This is important for Ethereum.
Like for a web service, attacker can be anywhere
Source code often available (good and bad)
Prominent example: The DAO