Andrei Voronkov, Iman Narasamdya
Proving Inter-Program Properties (2008)
Proving Inter-Program Properties (2008)
TR-2008-13.pdf
Keywords: Assertion Function, Invariant, Translation Validation, Common Criteria Certification
Abstract: We develop foundations for proving properties relating two programs. Our formalization is based on a suitably adapted notion of program invariant for a single program. First, we give an abstract formulation of the theory of program invariants based on the notion of assertion function: a function that assigns assertions to program points. Then, we develop this abstract notion further so that it can be used to prove properties between two programs. We describe two applications of the theory. One application is in the translation validation for optimizing compilers, and the other application is in the certification of smart-card application in the framework of Common Criteria. The latter application is part of an industrial project conducted at Verimag laboratory.
