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 post optimization 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. CACM July, 1978 Samet, H. Compilers, correctness, code optimization, debugging, program verification, Lisp 4.12 4.21 4.22 5.24 CA780708 DH February 7, 1979 3:53 PM 1024 4 3080 1051 4 3080 1102 4 3080 1132 4 3080 1390 4 3080 1486 4 3080 1549 4 3080 1706 4 3080 1826 4 3080 1878 4 3080 378 4 3080 2060 4 3080 2155 4 3080 2168 4 3080 2719 4 3080 2723 4 3080 2838 4 3080 2842 4 3080 2855 4 3080 2879 4 3080 3077 4 3080 3080 4 3080 3080 4 3080 3106 4 3080 627 4 3080 106 4 3080 210 5 3080 2850 5 3080 3080 5 3080 3080 5 3080 3080 5 3080