Access Restriction

Author Samet, Hanan
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Language English
Subject Keyword Code optimization ♦ Debugging ♦ Correctness ♦ Lisp ♦ Program verification ♦ Compilers
Abstract 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.
Description Affiliation: Univ. of Maryland, College Park (Samet, Hanan)
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2005-08-01
Publisher Place New York
Journal Communications of the ACM (CACM)
Volume Number 21
Issue Number 7
Page Count 13
Starting Page 570
Ending Page 582

Open content in new tab

   Open content in new tab
Source: ACM Digital Library