Como provar que seu código não tem erros de execução (e por que você provavelmente desistirá de tentar)
A interpretação abstrata permite provar que erros de execução são impossíveis antes da execução. Veja como ela funciona na prática, por que é difícil e onde se encaixa na sua cadeia de ferramentas.