Obwohl Programmiersprachen und Übersetzerkonstruktion diejenigen
Teilgebiete der praktischen Informatik sind, deren Theorien am besten
erforscht sind, kann man sich auf Übersetzer immer noch nicht voll
verlassen, insbesondere nicht bei realistisch-industriell eingesetzten
Programmiersprachen auf realen Prozessoren.  Zwei Gründe sind
hauptverantwortlich: Die Literatur zur Übersetzerverifikation
diskutiert nur die Korrektheit von Übersetzungsspezifikationen, wie
die ebenso erforderliche Korrektheit von Übersetzerimplementierungen
bis hinab zum binären Maschinencode. Diese Literatur geht auch nicht
auf die traditionell benutzten Architekturen realistischer Übersetzer
und Übersetzergeneratoren ein. Mit Blick auf realistische,
industrielle Anwendung sucht Verifix diese Lücken zu beseitigen, so
daß künftig auch in sicherheitskritischen Fällen kein niederer Code
mehr inspiziert werden muß.