VÉRIFICATION FORMELLE DES CONTRATS INTELLIGENTS
Dr. Christian Reitwiessner
@ethchris
github.com/chriseth
IC3-Ethereum Crypto Boot Camp
2016-07-26
Problème :
Écrire du code correctement est difficile !
Objectif clé : aligner le modèle mental avec le modèle machine
Facile de tester le comportement souhaité, difficile de vérifier l'absence de comportement indésirable
Raison : les tests ne couvrent qu'un nombre fini de cas
C'est important pour Ethereum.
Comme pour un service web, l'attaquant peut être n'importe où
Le code source est souvent disponible (bon et mauvais)
Exemple marquant : The DAO