Verified validation of lazy code motion
Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, pp. 316-326, 2009.
Translation validation establishes a posteriori the correctness of a run of a compilation pass or other program transformation. In this paper, we develop an efficient translation validation algorithm for the Lazy Code Motion (LCM) optimization. LCM is an interesting challenge for validation because it is a global optimization that moves c...More