Statische Analyse kann nicht beweisen, dass Ihr Flugzeug nicht abstürzt. Sie kann etwas Nützlicheres beweisen.
Die abstrakte Interpretation überapproximiert jeden möglichen Programmzustand. Wenn eine Division durch Null in der Abstraktion unerreichbar ist, ist sie im echten Code unerreichbar. So funktioniert sie – und hier zeigen sich ihre Grenzen.
Statische Analyse kann nicht beweisen, dass ein Flugzeug nicht abstürzt. Sie kann beweisen, dass die Regelschleife Ihres Höhenmessers niemals durch Null teilt,…