Статический анализ не может доказать, что ваш самолёт не разобьётся. Но он может доказать кое-что более полезное.
Абстрактная интерпретация аппроксимирует сверху каждое возможное состояние программы. Если деление на ноль недостижимо в абстракции, оно недостижимо и в реальном коде. Вот как это работает и где даёт сбои.
Статический анализ не может доказать, что самолёт не разобьётся. Но он может доказать, что контур управления высотомером никогда не поделит на ноль, никогда не…