Die Arbeit ist motiviert durch das Bestreben, im Rahmen der Projekte
  Verifix und VerComp eine erste voll verifizierte Implementierung
  eines Uebersetzers einer Teilsprache ComLisp von Common Lisp in den
  ausfuehrbaren Maschinencode eines realen Prozessors zu
  erreichen. ComLisp dient dabei als System- und insbesondere
  Uebersetzerimplementierungssprache und bietet vor allem dynamische
  Datentypen (S-Ausdruecke), die sich zur Implementierung abstrakter
  Programme bestens eignen. Korrekte Implementierung (Uebersetzung)
  von ComLisp geschieht in mehreren Phasen unter Benutzung
  verschiedener Zwischensprachen, so dass wesentliche Schritte separat
  und unabhaengig verifiziert werden koennen.

  Daten- und Operationsverfeinerung fuer S-Ausdruecke, ihre
  Konstruktoren, Selektoren und Praedikate findet sich in der
  Uebersetzung von SIL (einer Stack-Zwischensprache) nach Cint (einer
  maschinenorientierten Sprache mit linearem Speichermodell)
  wieder. Die Arbeit zeigt die Korrektheit der Implementierung der
  ComLisp-Operatoren (die auch SIL-Operatoren sind) im Sinne der
  Erhaltung partieller Korrektheit (L-Simulation). Es wird ebenfalls
  ein Stop-and-Copy-Speicherbereinigungsverfahren verifiziert.