Symbolic transfer function-based approaches to certified compilation

We present a framework for the certification of compilation and of compiled programs. Our approach uses a symbolic transfer functions-based representation of programs, so as to check that source and compiled programs present similar behaviors. This checking can be done either for a concrete semantic interpretation tion Validation) or for an abstract semantic interpretation (Invariant Translation) of the symbolic transfer functions. We propose to design a checking procedure at the concrete level in order ate both the transformation and the translation of abstract invariants. The use of symbolic transfer functions makes possible a better treatment of compiler optimizations and is adapted to the checking of precise invariants at the assembly level. The approach proved successful in the implementation point of view, since it rendered the translation of very precise invariants on very large assembly programs feasible. Categories and Subject Descriptors: D.2.4 [Software/Program Verification...

• Type: Conference
• Year: 2004
• Where: POPL
• Authors: Xavier Rival
• Keywords: POPL 2004, Present Similar Behaviors, Programming Languages, Semantic Interpretation, Symbolic Transfer Functions