VERIFICAÇÃO FORMAL DE CONTRATOS INTELIGENTES
Dr. Christian Reitwiessner
@ethchris
github.com/chriseth
IC3-Ethereum Crypto Boot Camp
2016-07-26
Problema:
Escrever código corretamente é difícil!
Objetivo principal: alinhar o modelo mental com o modelo da máquina
Fácil testar o comportamento desejado, difícil verificar a ausência de comportamentos indesejados
Razão: testes capturam apenas uma quantidade finita de casos
Isso é importante para o Ethereum.
Assim como para um serviço web, o atacante pode estar em qualquer lugar
O código-fonte geralmente está disponível (bom e ruim)
Exemplo proeminente: The DAO