We present a method for analyzing assembly programs obtained by compilation and checking safety properties on compiled programs. It proceeds by analyzing the source program, translating the invariant obtained at the source level and then by checking the soundness of the translated invariant with respect to the assembly program. This process is especially adapted to the certification of assembly or other machine-level kinds of programs. Furthermore, the success of the invariant checking enhance the level of confidence in the results of both the compilation and the static analysis. From the practical point of view, our method is generic in the choice of an abstract domain for representing sets of stores and the process does not interact with the compilation itself. Hence, a certification tool can be interfaced with an existing analyzer and designed so as to work with a class of compilers which do not need to be modified. Last, a prototype was implemented in order to validate the approach.

@Article{I-xr_sttt_2004,
  author =       {X. Rival},
  title =        {Invariant Translation-Based Certification of Assembly Code},
  journal =      {International Journal on Software and Tools for Technology Trasnfer},
  year =         {2004},
  OPTkey =       {},
  volume =       {6},
  number =       {1},
  pages =        {15--37},
  month =        {july},
  OPTnote =      {},
  OPTannote =    {},
}