Formal Verification of Smart Contracts: Dr. Christian Reitwiessner – IC3-Ethereum Crypto Boot Camp



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

source

Related posts

Leave a Comment