In diesem Vortrag beschreiben wir die mathematischen Grundlagen und
Einsatzmöglichkeiten der Technik der Programmprüfung und der
checker-basierten Programmverifikation zur Übersetzerverifikation im
Rahmen des Verifix-Projektes. Programmprüfung basiert auf
Laufzeitprüfung von Nachbedingungen eines Programms oder Programmteils
durch hinreichende algorithmische Formulierungen von
Korrektheitsprädikaten.  Checker-basierte Programmverifikation ist
eine Technik zur vollen Verifikation der partiellen Korrektheit, die
Laufzeitprüfung ausnutzt und eine Modularisierung des Programms in
einen (häufig großen) unkritischen Teil und kritische, zu
verifizierende Prüfroutinen erlaubt. Letztere lassen sich geradlinig
induktiv formulieren und leichter verifizieren. In einem Beispiel
zeigen wir im zweiten Teil Definition und Verifikation der Korrektheit
der Analysephase mit lexikalischer, syntaktischer und semantischer
Analyse auf der Basis von Attributgrammatiken. Andere Beispiele auch
außerhalb des Übersetzerbaus werden kurz skizziert.