El análisis estático no puede demostrar que tu avión no se estrellará. Puede demostrar algo más útil.
La interpretación abstracta sobreaproxima cada posible estado del programa. Si una división por cero es inalcanzable en la abstracción, es inalcanzable en el código real. Así es como funciona y dónde falla.
El análisis estático no puede demostrar que un avión no se estrellará. Sí puede demostrar que el bucle de control del altímetro nunca dividirá por cero, nunca…