Dieser Vortrag gibt einen Überblick über die aktuellen Arbeiten im
Bereich maschinell-unterstützter Verifikation der Transformation und
Implementierung. Wir stellen einen generischen Ansatz zur formalen
Spezifikation und Verifikation prozeduraler Programme vor, der von
konkreten Übersetzungsprozessen abstrahiert, indem das Wesentliche
eines Übersetzungsschrittes identifiziert und abstrakt modelliert
wird.  Ein solcher Ansatz erlaubt eine für die Durchführbarkeit
maschineller Beweise adäquate vertikale und horizontale
Modularisierung. Der Ansatz wird mit Hilfe generischer PVS-Theorien
für einzelne Sprachkonstrukte und Übersetzungsschritte realisiert, die
mit den jeweils relevanten Komponenten des Übersetzungsschrittes
parametrisiert sind. Backend-Spezifikation bestehen aus einer Menge
von Regelschemata, die Zwischensprachtermen Zielcode zuordnen. Wir
stellen vor, wie solche Spezifikationen mit Hilfe spezialisierter
PVS-Strategien vollautomatisch formal verifiziert werden können. Bei
der Implementierungsverifikation verfolgen wir einen konstruktiven
Ansatz, bei welchem ein Übersetzerprogramm durch Anwendung
semantik-erhaltender Transformationen aus der
Übersetzungsspezifikation generiert wird. Es wurde hierzu ein formaler
Rahmen in PVS entwickelt, der die Integration von
Entwicklungsschritten und Transformationen aus unterschiedlichen
transformationellen Ansätzen erlaubt. Die Anwendung des formalen
Rahmens wird am Beispiel der Konstruktion eines Übersetzers von
ComLisp nach SIL illustriert.