Translation Validation: Automatically Proving the Correctness of Translations Involving Optimized Code
Hanan Samet · 2012
Definition: a means for proving for a given compiler (or any program translation procedure) for a high level language H and a low level language L that a program written in H is successfully translated to L Motivation is desire to prove that optimizations performed during the translation process are correct 1. Often, optimizations are heuristics 2. Optimizations could be performed by simply peering over the code Proof procedure should be independent of the translation process (e.g., compiler) Notion of correctness must be defined carefully Need a representation that reflects properties of both the high and low level language programs 1. Critical semantic properties of high level language must be identified 2. Identify their interrelationship to instruction set of computer executing the resulting translation