Verifizierte Übersetzer sind essentiell für die Entwicklung
sicherheitskritischer Softwaresysteme. Kritische Teile von
Steuersystemen werden immer noch auf Assemblerebene geschrieben und
verifiziert, da Übersetzer für Hochsprachen nicht als vertrauenswürdig
angesehen werden. Für industrielle Anwendungen müssen die Techniken
zur Konstruktion korrekter Übersetzer einfach anzuwenden und in den
Softwareentwicklungsprozeß einzubinden sein. So entstehen nicht nur
algorithmische Probleme der Verifikation, sondern auch
Architekturprobleme der Konstruktion verifizierter Übersetzer gemäß
aktueller Softwareentwicklungsstandards. Wir zeigen, daß Spezifikation
und Verifikation in die traditionelle Übersetzerarchitektur integriert
werden können. Diese Integration reduziert sowohl die Komplexität, als
auch den Umfang der Verifikation.