FORMAL VERIFICATION OF SMART CONTRACTS
Slides – https://chriseth.github.io/notes/talks/formal_ic3_bootcamp/#/
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
