In der zweiten Zweijahresprojektphase ist Verifix einen überzeugenden
Schritt hin zu einer ingenieurmäßigen und industriell einsetzbaren
Technik zur Entwicklung und Konstruktion voll verifizierter,
realistischer Übersetzer und Übersetzergeneratoren für realistische
Programmiersprachen auf realen Prozessoren gelungen. Volle
Verifikation heißt, daß auch Übersetzer und Übersetzergeneratoren, die
als ablauffähige, binäre Maschinenprogramme realer Prozessoren
implementiert sind, lückenlos als korrekt eingesehen und bewiesen
werden können. Hervorzuhebendes Verifix-Merkmal ist, daß
praktisch-industriell bewährte Entwicklungsmethoden für Übersetzer und
Generatoren beibehalten werden; die Verifikation wird in
modular-additiver Weise draufgesattelt. Das ist möglich geworden durch
systematisches Einsetzen der Idee der Programmprüfung (Beweis durch
Probemachen, result-checking, speziell sog. Codeinspektion). In der
Projektausschreibung "Werkzeug zur Analyse von Objectcode und von
optimierenden Übersetzern -- OCOCAT", 1996, hat das Bundesamt für
Sicherheit in der Informationstechnik BSI festgestellt:

   Jedes Software-Herstellungsverfahren hat zwei Brüche
   (Sicherheitslücken) in lückenloser, konsistenter Überprüfbarkeit:
   Übergang von Softwareentwurf zu hochsprachlichem Quellcode, und von
   dort zu integriertem, ablauffähigem, binärem Maschinencode. OCOCATs
   Anliegen ist die Sicherheitslücke 2., d.h. das bisher nicht
   erreichte, voll korrekte, realistische Übersetzen.

Das aber ist gerade auch das Anliegen von Verifix. Es ist
bemerkenswert, daß das BSI die Sicherheitslücke 2.  jetzt anerkannt
hat. Das war vor zehn Jahren in der Definitionsphase des BSI-Projekts
``VSE -- Verification Support Environment'' noch nicht so, weshalb der
Vortragende mit seinen Vorschlägen damals nicht auf Resonanz beim BSI
gestoßen war. Mit dem erfolgreichen Einsatz der Technik des
Programmprüfens im voll korrekten realistischen Übersetzerbau zeigt
Verifix Perspektiven auf, wie im generellen Softwareengineering
existierende Software weiterverwendet werden kann. Ferner ist
hervorzuheben, daß Programmiersprachen und Übersetzerbau dasjenige
praktische Informatikgebiet ist, das am stärksten von Theorie
durchdrungen ist. Die Mitstreiter in Verifix sind sich einig, daß vor
allem deshalb der Bau voll korrekter, realistischer,
industrierelevanter Übersetzersoftware gelingen kann. Es ist zu
hoffen, daß auch anderen praktischen Informatikbereichen eine ähnliche
Durchdringung mit Theorie gelingt.