Paleri, VK.  2002.  Automatic Generation of Code Optimizers from Formal Specifications. The Compiler Design Handbook. :61-97.