Proving the correctness of heuristically optimized code

A system for proving that programs written in a high level language are correctly translated to a low level language is described. A primary use of the system is as a postoptimization step in code generation. The low level language programs need not be generated by a compiler and in fact could be hand coded. Examples of the usefulness of such a system are given. Some interesting results are the ability to handle programs that implement recursion by bypassing the start of the program, and the detection and pinpointing of a wide class of errors in the low level language programs. The examples demonstrate that optimization of the genre of this paper can result in substantially faster operation and the saving of memory in terms of program and stack sizes.

View this article in the ACM Digital Library.