Formal Verification

Wo ein Fehler Milliarden kostet oder Menschen tötet:

• Chips (CPU): Intel verifiziert jede Gleitkomma-Einheit (nach dem Pentium-Bug Desaster).
• Raumfahrt (NASA): Mars Rover Software.
• Krypto: Blockchain Smart Contracts (wo Bugs Millionen klauen).
• Züge/Flugzeuge: Steuerungssoftware. Für normale Apps (Webseiten) ist es (noch) zu teuer.

1. Model Checking vs. Theorem Proving

Die zwei großen Schulen.

• Model Checking (Automatisch): Sucht den Zustandsraum ab (NuSMV, SPIN). Limitiert durch "State Explosion".
• Theorem Proving (Manuell): Beweist Sätze logisch (Coq, Isabelle). Unendlich mächtig, aber braucht Experten-Gehirnschmalz.

2. Static Analysis

Die "kleine Schwester". Tools wie Coverity oder SonarQube suchen nach Mustern ("Hier könnte Nullpointer sein"). Das ist keine volle Verifikation (es gibt False Positives/Negatives), aber im Alltag viel nützlicher.

1. SMT-Solvers (The Engine under the Hood)

Hinter fast allen modernen Verifikationstools (Dafny, Frama-C, CBMC) steckt ein SMT-Solver (Satisfiability Modulo Theories), meistens Z3 oder CVC5. Ein SMT-Solver ist ein "Super-Rechner" für Logik. Er versteht nicht nur WAHR/FALSCH, sondern auch ganze Theorien wie:

• Arithmetik: Er weiß, dass $x+1 > x$ immer gilt.
• Arrays: Er versteht den Unterschied zwischen Index und Wert.
• Bit-Vektoren: Er kennt Overflows bei 32-Bit Integers. Wenn ein Verifikationstool deinen Code prüft, übersetzt es die Programmlogik in eine gigantische mathematische Formel und fragt den SMT-Solver: "Gibt es IRGENDEINE Belegung der Variablen, die diese Assertion verletzt?". Findet der Solver nichts, ist der Beweis erbracht.

2. Operational vs. Axiomatic Semantics

Damit man Software beweisen kann, muss man erst definieren, was "Software" mathematisch überhaupt ist.

• Operational Semantics: Beschreibt, wie eine virtuelle Maschine den Code Schritt für Schritt ausführt (Zustandsübergänge). Gut für Model Checker.
• Axiomatic Semantics (Hoare Logic): Beschreibt den Code durch Vor- und Nachbedingungen. {Pre} Code {Post}. Das ist die Basis für deductive Verifikation ( Theorem Prover). Man beweist nicht den Lauf des Programms, sondern die Transformation der logischen Wahrheit durch den Code.

3. Soundness vs. Completeness (The Trade-off)

In der Forschung kämpft man mit der Unentscheidbarkeit. Ein Tool ist Sound (Sicher), wenn es jeden Fehler findet (keine False Negatives), aber vielleicht manchmal Alarm schlägt, obwohl alles okay ist (False Positives). Ein Tool ist Complete (Vollständig), wenn jeder Alarm auch wirklich ein Fehler ist. Wegen Gödels Unvollständigkeitssatz können wir für komplexe Sprachen (wie C++) nie beides gleichzeitig haben. Formale Verifikation wählt fast immer Soundness: Es ist besser, den Entwickler einmal zu viel zu nerven, als einen Bug zu übersehen, der später zum Absturz des Satelliten führt.