Proving Program Properties in Translation Validation

We develop foundations for proving equivalence and other properties of programs in translation validation. Our formalisation is based on a suitably adapted notion of program invariant.

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 in translation validation. We show that the resulting theory can be used to validate compilation.