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