We present a method for analyzing assembly programs based on source program analysis and invariant translation. It is generic in the choice of an abstract domain for representing stores. This method is adapted to the design of certification tools for assembly programs generated by compiling programs written in an imperative language, without writing a specific compiler or modifying an existing one since invariant translation only uses standard debugging information. A prototype was developed for a procedural subset of the C language.

@InProceedings{I-xr_vmcai_2003,
  author =       {X. Rival},
  title =        {Abstract interpretation-based certification of assembly code},
  booktitle =    {4th Conference on Verification, Model Checking
                  and Abstract Interpretation},
  pages =        {41--55},
  year =         {2003},
  editor =       {L. Zuck et al},
  volume =       {LNCS 2575},
  month =        {janvier},
}