Soll ein Softwaresystem verifiziert implementiert werden, muß entweder
direkt auf Ebene der Zielmaschine überprüft werden, oder aber ein
verifizierter Übersetzer für die eingesetzte Hochsprache vorhanden
sein.  Unser Ziel ist es, verifiziert implementierte Übersetzer zu
konstruieren, die effizienten Code für gängige Sprache erzeugen. Der
Codegenerator ist gemäß unserer Architektur der Teil eines
Übersetzers, der die Transformation in konkrete Maschineninstruktionen
vornimmt. Sollen praktisch relevante Übersetzer konstruiert werden,
müssen auch praktisch erprobte und effiziente Verfahren eingesetzt
werden. Dies betrifft sowohl Optimierungstechniken als auch die
Transformationsschritte selber. Im Übersetzerbau haben sich
Termersetzungssysteme als Mechanismus für diesen Transformationsschritt
bewährt. Neben globalen Bedingungen an das Termersetzungssystem (siehe
Zimmermann) fallen bei der Verifikation einzelner Ersetzungsregeln
lokale Beweisverpflichtungen an. Diese sind hochgradig sprachabhängig,
fallen in großer Anzahl an und sind zudem sehr fehleranfällig. Wir
zeigen, wie diese Regeln systematisch durch Simulationsbeweise
verifiziert werden können und wie mechanische Beweisunterstützung
Fehler finden hilft, und geben einige Beispiele.