Translation Validation: Automatically Proving the Correctness of Translations Involving Optimized Code

Speaker:  Hanan Samet – College Park, MD, United States
Topic(s):  Software Engineering and Programming

Abstract

An early 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.  It can also be used to demonstrate the correctness of a bootstrapping process and can be viewed as being in the realm of compiler testing.  Using today's terminology this work falls in the realm of translation validation although the supporting research was carried out 25 years earlier in the 1970s.  The low level language programs need not be generated by a compiler and in fact could be hand code.  Examples of the usefulness of such a system are given in the context of LISP and a suitably chosen assembly language. 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 such optimizations can result in substantially faster operation and the saving of memory in terms of program and stack sizes. 

About this Lecture

Number of Slides:  38
Duration:  60 minutes
Languages Available:  English
Last Updated: 

Request this Lecture

To request this particular lecture, please complete this online form.

Request a Tour

To request a tour with this speaker, please complete this online form.

All requests will be sent to ACM headquarters for review.