To appear in Proceedings of the 17th European Symposium on Programming (ESOP), Budapest, Hungary, 2008. LNCS, (c) Springer-Verlag.

Gilles Barthe and César Kunz
INRIA Sophia-Antipolis, Project EVEREST.

Abstract. A certificate is a mathematical object that can be used to establish that a piece of mobile code satisfies some security policy. Since in general certificates cannot be generated automatically, there is an interest in developing methods to reuse certificates. This article formalises in the setting of abstract interpretation a method to transform certificates of program correctness along program transformations.