Safety critical software crucially depends on the methods and tools
  used in their construction process. In the project Verifix we focus
  on compilers which are used as tools to translate safety critical
  programs from a source language to machine code of a target
  processor.  Correct compiler operation is required to assert quality
  properties about the machine program (and thus the whole system)
  which ultimately runs in the application.  We follow accepted
  software engineering phase models to construct our compilers, so
  compiler correctness has to be proved on different levels in the
  compiler construction process.  Three main levels turned out to be
  reasonable.  First, even traditional compiler construction theory
  asks the question, if a mathematically defined translation function,
  which maps from source language programs to target language
  programs, respects their semantics. We call the process of proving
  its correctness compiling specification verification.  Second, we
  have to answer the question whether a compiler programmed in a given
  implementation language is indeed a correct implementation of the
  translation function (correct compiler program construction).  On
  the third level, we need to have the evidence that the ultimately
  resulting compiler program in machine code is a valid implementation
  of the compiler program in implementation language (correct compiler
  implementation). Thus we consider compilers for safety critical
  systems to be safety critical software themselves.  Because any
  automatism raises the question of correct machine code
  implementation again, the third step must be performed semi
  automatically at least once and has to be based on manual
  mathematical proofs. This article shows a proof technique for
  correct compiler implementation verification. It is based on a
  bootstrapping technique with afterwards control steps. This allows
  to conclude a correct compiler implementation in machine code
  without inspecting the whole generation process.  In contrast to
  contemporary believe, a correct compiler implementation can in deed
  be gained with acceptable effort.