Sorin Lerner, Todd D. Millstein, Craig Chambers. Automatically proving the correctness of compiler optimizations. In Proceedings of the ACM SIGPLAN 2003 Conference on Programming Language Design and Implementation 2003, San Diego, California, USA, June 9-11, 2003. pages 220-231, ACM, 2003. [doi]