Symbolic transfer function-based approaches to certified compilation

9 years 10 months ago
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...
Xavier Rival
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2004
Where POPL
Authors Xavier Rival
Comments (0)