This thesis is concerned with the problem of correct implementation
  of programming language compilers in high level implementation
  language and binary machine code of real processors.

  It proposes a new and practicable method to assure full correctness
  of the implementation for an initial compiler. This compiler works
  in several compiler phases which generate intermediate results in
  intermediate languages. Starting from compiling specifications
  assumed to be correct, compiler programs are constructed in a high
  level implementation language (correct compiler construction) which
  is also source language of the first phase and sublanguage of an
  existing programming language. In order to assure correct
  implementation in binary machine code as well (compiler
  implementation verification) the compiler programs are translated in
  a bootstrapping process (the compiler programs compile their own
  program representations) from high level implementation language to
  binary machine code. For the source--, intermediate-- and
  target--language fragments generated in this process a rigorous
  syntactical code inspection takes place. For this purpose,
  corresponding fragments are displayed juxtapose and are
  syntactically compared based on mathematically founded check
  criteria.  Successful code inspection assures that the translation
  has been performed according to the specification and thus that it
  has been correct. The compiler is then correctly available in
  machine code.

  Because of the special compiler structure it is not necessary to
  inspect all compiler phases at all intermediate language
  levels. Under the assumption that the executing processor is
  correct, phases already accepted to be correct can be used to
  correctly generate further compiler phases. The translation of a
  phase must be inspected only down to its target language which
  drastically reduces the inspection effort.

  Result of the compiler implementation verification is a full set of
  proof protocols which completely document the machine code
  implementation. If despite verification errors occur later then this
  documentation can be used to precisely locate their causes. In this
  sense the proof protocols are example for the certification of other
  safety or security critical systems. In contrast to classical code
  inspection which examines programs semantically, the proposed method
  is completely of syntactical nature, i.e. understanding why the
  inspected translation is correct is not strictly necessary.

  As long as no fully verified compilers exist, the correctness of
  ultimately executed machine code for programs can not be assured by
  reasoning at source code level alone.

  This thesis solves this problem for a compiler itself and so makes
  an important step towards full correct programs.