Symbolic Transfer Function-based Approaches to Certified Compilation

Xavier Rival

To appear at Principles of Programming Languages (POPL04), Venice, Italy, January 14-16, 2004


Abstract

We present a framework for certifying compilation and 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 (Translation 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 to validate 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.


Server START Conference Manager
Update Time 19 Sep 2003 at 17:40:43
Maintainer Xavier.Leroy@inria.fr.
Start Conference Manager
Conference Systems